Higher-Order rules : documentation

[francoisthire]

Trying to test lambdapi on example #59 , I found that documentation was missing for HO rules.

I have the impression that the correct syntax (right now) is:

A : Type.

a : A.

def f : (A -> A) -> A.

f (x => ?y[x]) --> a.

However, the following syntax is rejected not at parsing level (btw the error message could be improved):

(; KO 9 ;)

A : Type.

a : A.

def f : (A -> A) -> A.

[y] f (x => ?y[x]) --> a.

While the example below is rejected at parsing level:

A : Type.

a : A.

def f : (A -> A) -> A.

[y] f (x => y[x]) --> a.

At least we should have a note that explain the differences between the syntax of Dedukti and the one of lambdapi.

[rlepigre]

Well, you should not be able to mix the legacy syntax with the actual lambdapi syntax. I'll check what I can do to reject the last two examples, and document the syntax properly.

[rlepigre]

There is no bug here (any more?), only missing documentation. The first example uses the (correct) new syntax. The second example attempts to mix legacy syntax with new syntax, which is rejected at scoping type with an adequate error message (pointing to the position of the ?y[x] subterm). Finally, the last example is simply not syntactically correct: y[x] has no meaning in either the legacy and the new syntax.

[francoisthire]

Maybe the file "newRuleSyntax.dk" should be renamed so that it is easier to understand that it is about Higher-Order patterns.

[fblanqui]

@rlepigre : can't we close this issue?

[rlepigre]

@fblanqui: I guess so.