Frédéric Blanqui
Frédéric Blanqui
I don't understand why I get a parsing error with: ``` def Set : Type. injective {|τ|} : (Set -> Type). def {|ℕ|} : Type. def 0 : {|ℕ|}. def...
Would it be possible to add an option (say -w/--no-warnings) for not printing warnings? E.g. "[Warning] Trying to import the already loaded module ..."
It would be helpful to be able to declare some theorems as local (private in lambdapi syntax) so that there are not visible outside the file and thus not included...
With big files containing millions of identifiers, module prefixes can take a lot of disk space. An easy way to reduce this is to use module aliases, that is, to...
dk dep takes more than 11 minutes to compute the dependencies of the 111 dk files generated by isabelle_dedukti for the HOL standard library. This is more than the time...
it returns "%%VERSION%%"
Please do not merge this PR but keep it open: its purpose is to provide data on working ocaml-camlp5 pairs. It contains some github action scripts to inventory the pairs...
Hi. Is there any plan to have hol-light working with recent versions of ocaml and camlp5? See https://github.com/jrh13/hol-light/pull/71.
Hello. Using ocaml.4.02.3 and campl5.6.17 I get the following problem: ``` #use "hol.ml";; # module OrdInt = struct type t = int let compare = (-) end;; Toplevel input: #...
The Makefile generated by lambdapi init is not that nice since it is calling lambdapi only once with all the files as argument so that files are not checked in...