Incorrect ident parsing in transformations
In each of the following examples, the output of print (+)
is function (+) real real: real
and (in M1) cut (0 + 0 = 0)
fails with a typing error, when (+) should be the integer addition :
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
Maybe the use import real.Real
declaration in RealInfix
is treated as a use export
?