Re: [isabelle] Syntax for existential equation
I am not sure where the syntax =e= comes from, but it is not part of HOL.
Michael Chan schrieb:
> Is the following using the correct syntax for existential equation? I found
> it somewhere, but ProofGeneral seems to not like it.
> axioms ga_function_monotonicity_25 [rule_format] :
> "ALL x1.
> ALL x2. gn_inj_Nat_Int(x1) mod' gn_inj_Nat_Int(x2) =e= x1 mod'' x2"
> *** Type unification failed: Clash of types "*" and "bool"
> *** Type error in application: Incompatible operand type
> *** Operator: op = (gn_inj_Nat_Int(x1) mod' gn_inj_Nat_Int(x2) = e) :: bool
> => bool
> *** Operand: x1 mod'' x2 :: bool * X_Nat
> *** The error(s) above occurred in axiom "ga_function_monotonicity_25"
> *** At command "axioms".
> It seems that the 'e' in =e= is parsed as a variable.
This archive was generated by a fusion of
Pipermail (Mailman edition) and