package rocq-runtime
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824
doc/rocq-runtime.coqdeplib/Coqdeplib/File_util/index.html
Module Coqdeplib.File_utilSource
to_relative_path path takes as input a file path path, and constructs an equivalent relative path from the current working directory. If path is already relative, then it is returned immediately.
normalize_path path takes as input a file path path, and returns an equivalent path that: (1) does not contain the current directory member "." unless the path is to the current directory (in which case "." is returned, or "./" if path has a trailing "/"), (2) only uses parent directory members ".." for a prefix of the path, and (3), has a trailing "/" only if and only if path does.
For example, paths "dir1/dir2/file.v", ".", "dir1/dir2/dir3/" and "../../dir/file.v" are possible return values, but "./file.v" and "dir1/../dir2" are not.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>