aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorJason Gross2019-05-22 17:13:24 -0400
committerJason Gross2019-05-22 21:15:02 -0400
commitcd6db46a88eb192b7370308489cd4e2b719df342 (patch)
treee2cee90d62edb0f65569a90b11a938fa27f5bf52 /kernel/cemitcodes.ml
parent5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff)
[Ltac2] Add util files for Bool, List, Option
Most functions are taken either from the Coq standard library or the OCaml standard library. One (`enumerate`) is taken from Python. Most names are chosen according to OCaml conventions (as Coq does not have exceptions, and so the OCaml naming conventions already distinguish between option and exception). Since `exists` is a keyword, we use the Coq name `existsb` instead. We generally favor Coq argument ordering when there is a conflict between Coq and OCaml. Note that `seq` matches neither Coq nor OCaml; it takes a `step` argument for how much to increment by on each step. Sorting functions are mostly taken from Coq's mergesort library; it might make sense to replace them with OCaml's versions for efficiency?
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions