package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.coqdeplib/Coqdeplib/File_util/index.html
Module Coqdeplib.File_util
Source
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)"
>