Frédéric Blanqui

There are a few problems with ";": - the parser and the printers are not consistent on metavariable arguments: the parser uses ";" and the printers "," - ";" is...

Remove Parser.lp_lexbuf_fixup ?

2

introduced in #552

Example: x:A:=a |- t = u.

Record the list of variables with their types in typing rules ?

1

This field would be set after checking subjection reduction. This would simplify termination and confluence checking. Note that it is important that termination and confluence checking is fast. Otherwise people...

Error in HRS output

1

In a rule LHS, type annotations of abstractions are replaced by the *same* variable m_typ: https://github.com/Deducteam/lambdapi/blob/82dccc5074bd42574d8d21b9b39527052d2014cd/src/core/hrs.ml#L38

The Makefile generated by LP stops at the first error even with the option -k

16

We currently have no tools to compile a set of LP files. If in your project you have two files a.lp and b.lp with a.lp depending on b.lp, then a.lp...

Add notations with place-holders

1

@rlepigre proposes to define notations with « place-holders » with priorities like: - "if _ then _ else _", - "_ ⊢ _ : _", _ "⟦ _ ⟧", -...

Do not check that a module name is a keyword

9

https://github.com/Deducteam/lambdapi/blob/3b25ff1cfec2b65f37a9199c349eeded7f3888d3/src/parser.ml#L238 Currently a module name must be any_ident, that is, an escaped_ident or a regular_ident but regular_ident must be different from keywords: https://github.com/Deducteam/lambdapi/blob/3b25ff1cfec2b65f37a9199c349eeded7f3888d3/src/parser.ml#L223 This exclude filenames like set, simpl, intro,...

Add pattern matching modulo eta ?

1

Currently, the following file is not accepted: ``` symbol R:TYPE symbol sin:R⇒R symbol D:(R⇒R)⇒(R⇒R) rule D(λx,sin &F[x]) → λx:R,x assert D sin ≡ λx:R,x ```

Incorrect use of Unicode symbol in error message for Coq

1

With the following code: ``` Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. Scheme paths_ind := Induction for paths Sort...