Frédéric Blanqui

TODO: - [X] add axioms for AC symbols - [ ] update doc - [ ] start function symbol names by a lowercase letter - [ ] replace unicode characters...

When scoping rule LHS of AC symbols, AC-canonization should be deactivated.

``` symbol a:A; symbol f : A → A → A; symbol i:A → A; symbol lem : A ≔ begin apply f { print ?1 } { }; end;...

`lambdapi check --lib-root=. foo.dk` fails when there is a `lambdapi.pkg` file with `path_root=foo`.

``` symbol 1000000000000000000000000000 : TYPE; symbol foo: 1000000000000000000000000000; [/home/blanqui/src/lambdapi/tmp/toobig.lp:2:12-40] Too big number (max is 4611686018427387903). ``` This is a problem in the parser. In terms, natural numbers are parsed as...

useful example: \/ used in hol-light

When a proof is aborted, the admitted goals (tactic admit) are kept in the signature.

``` A:Type. a:A. def f:A -> A. [] (f _) --> a. [ERROR CODE:702] [foo.dk] [line:4 column:3] Parsing error: Unexpected token '('. ```

``` def A : Type. def a : A. thm b := a. [ERROR CODE:702] [zo.dk] [line:3 column:6] Parsing error: Unexpected token ':='. ```

``` 16:54 /tmp/export_raw_dk ls tests_OK_1006.dk tests_OK_empty.dk tests_OK_1035.dk tests_OK_Escaped.dk tests_OK_225.dk tests_OK_eta_equality.dk tests_OK_262_pair_ex_1.dk tests_OK_for_inductive.dk tests_OK_292.dk tests_OK_freevars-constraints.dk tests_OK_301.dk tests_OK_identifiers.dk tests_OK_303.dk tests_OK_implicitArgs1.dk tests_OK_330b.dk tests_OK_implicitArgs2.dk tests_OK_330.dk tests_OK_nested_comment_lp.dk tests_OK_621c.dk tests_OK_patt.dk tests_OK_698_abst_impl.dk tests_OK_private.dk tests_OK_725.dk tests_OK_require_symbol.dk tests_OK_878.dk tests_OK_symbol.dk...