Email Gateway (Aug 18 2022 at 13:09): Email Gateway (Aug 18 2022 at 13:09):From: Michael Chan <dayzman@gmail.com>
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
Email Gateway (Aug 18 2022 at 13:09):From: Tobias Nipkow <nipkow@in.tum.de>
I am not sure where the syntax =e= comes from, but it is not part of HOL.
Regards
Tobias
Michael Chan schrieb:
Last updated: May 03 2024 at 08:18 UTC