lambdapi
lambdapi copied to clipboard
Escaped identifiers are not allowed for bound variables
Is this issue still open?
symbol A: TYPE;
symbol f : A → A → A;
symbol {|i$|}:A;
injective symbol + : A → TYPE;
opaque symbol test: Π {|i@|}, + (f {|i@|} {|i@|}) ≔
begin
assume {|i@|};
admit //...
end;
Escaped identifier sounds to work for bound variables, or maybe we are not speaking about the same thing.
Strange. You do not get an error?
13:28 ~/lambdapi (master) lambdapi check tmp/946.lp
Checking "/home/blanqui/src/lambdapi/tmp/946.lp" ...
[/home/blanqui/src/lambdapi/tmp/946.lp:6:22-28] "{|i@|}": Escaped identifiers or regular identifiers having an integer suffix with leading zeros are not allowed for bound variable names.
Which version of lambdapi do you use?
Oh sorry I forgot that I was in Lambdapi version: dev-2.1.0-116-g93668def because of #843,
so I also got the error
"{|i@|}": Escaped identifiers or regular identifiers having an integer suffix with leading zeros are not allowed for bound variable names.