Re: [isabelle] Syntax for existential equation



I am not sure where the syntax =e= comes from, but it is not part of HOL.

Regards
Tobias

Michael Chan schrieb:
> Hi,
> 
> 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.
> 
> Thanks.
> 
> Michael





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.