package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.lib/Util/index.html
Module Util
Source
This module contains numerous utility functions on strings, lists, arrays, etc.
Mapping under pairs
Folding under pairs
Equality on pairs
Mapping under triplets
Projections from triplets
Chars.
Empty type
Strings.
Substitute %s in the first chain by the second chain
Lists.
Arrays.
Sets.
Maps.
Matrices.
Functions.
Left-to-right function composition:
f1 %> f2
is fun x -> f2 (f1 x)
.
f1 %> f2 %> f3
is fun x -> f3 (f2 (f1 x))
.
f1 %> f2 %> f3 %> f4
is fun x -> f4 (f3 (f2 (f1 x)))
etc.
Delayed computations.
try_finally f x g y
applies the main code f
to x
and returns the result after having applied the finalization code g
to y
. If the main code raises the exception exn
, the finalization code is executed and exn
is raised. If the finalization code itself fails, the exception returned is always the one from the finalization code. Credit X.Leroy, D.Remy.
Enriched exceptions
Misc.
Alias for Union.map
Open an utf-8 encoded file and skip the byte-order mark if any.
A trick which can typically be used to store on the fly the computation of values in the "when" clause of a "match" then retrieve the evaluated result in the r.h.s of the clause