lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard

Escaped identifiers are not allowed for bound variables

Open fblanqui opened this issue 3 years ago • 3 comments

fblanqui avatar Jan 27 '23 20:01 fblanqui

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.

NotBad4U avatar Jul 10 '23 14:07 NotBad4U

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?

fblanqui avatar Jul 11 '23 11:07 fblanqui

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.

NotBad4U avatar Jul 11 '23 14:07 NotBad4U