Frédéric Blanqui
Frédéric Blanqui
@yannl35133 What is the status of this issue? You didn't answer my question yet.
@Rehan-MALAK @gabrielhdt what is the status of this PR? Thanks to tell me when it will be ready to merge.
The problem is in https://github.com/Deducteam/lambdapi/blob/42a0313bc81a7092ad7988cf7ac7f5006a9b41d4/src/compile.ml#L64 . Instead, Dedukti reads files line by line: https://github.com/Deducteam/Dedukti/blob/49e445420885c11b75d161735258ccef19ca2153/parsing/parser.ml#L17-L20 .
@01mf02, could you please provide an URL towards your file so that we can have a look at it?
Hi @01mf02 . I see that, in your big file, you use `definition proofXXX : A := p` for what looks like proofs. Couldn't you instead do the following: `theorem...
@rlepigre Before we get your new parser, could you please upgrade the current version of Earley so that we can compile LP with the most recent version of OCaml? It...
Fixed in #516 except in the LSP server.
The problem is that `foo/bar` is parsed as 3 separate identifiers `foo` `/` `bar` because `/` is not allowed in identifiers except as a single-letter identifier. I agree that the...
To solve this issue, I would rather suggest to do: ``` let separ_letter = [%sedlex.regexp? Chars " ,;.:\r\t\n(){}[]\""] let special_letter = [%sedlex.regexp? Chars "`@/|$?"] let forbidden_letter = [%sedlex.regexp? separ_letter |...
Coq and Agda use http://sphinx-doc.org/ for generating their doc. It looks really nice. We could use this techno as well.