Dedukti
Dedukti copied to clipboard
Free variable applied in LHS
For the file
nat : Type.
def pair : (nat->nat)->nat->nat.
def split : nat->nat.
[F,Y] split (F Y)-->pair F Y.
which should obviously be refused by Dedukti since F
is a free variable applied in the left-hand side of a rule, the error message is:
ERROR line:4 column:15 The variable 'Y[0]' was not found in context:
which is not informative at all.
@Gaspi , any plan to solve this?