lambdapi

lambdapi copied to clipboard

By @QGarchery: ``` symbol test_rew_lambda f : π (`∀ a, `∀ b, f (a + b) ⇒ f b) ≔ begin // Does not rewrite under binders rewrite add_com; end;...

fblanqui

Declare injectivity on some arguments only

6

This seems to be a better place to discuss the following issue: Deducteam/Dedukti/issues/151 ### Problem Consider the following example encoding an `even` predicate on natural numbers: ``` // Encoding symbol...

Gaspi

Hierarchy of tests

6

This PR is about the hierarchy of tests (Issue #487 ). More details should be discussed.

amelieled

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

fblanqui

Remove Parser.lp_lexbuf_fixup ?

2

introduced in #552

fblanqui

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

fblanqui

Goto definition ignores qualifier

4

In file tests/OK/PrintB.lp ``` symbol f:B→B→B compute a+a // should print a+a compute tests.OK.PrintA.f a a // should print a+a ^ ``` Goto definition goes to the `f` defined in...

firewall2142

Just to delete 3 functions (and test the new CI).

amelieled

LSP server: parse and check commands one by one

16

The current behavior of lambdapi is: 1. parse the file to generate a list of entries, 2. type check the file. This is becoming an issue with the importation of...

francoisthire

[POC] run Elpi code in lambdapi

10

*do not merge* this is a POC to be discussed at a seminar on the 18th TODO (hopefully for the 18th): - [x] support `Terms.Meta` in the HOAS encoding using...

gares