Email Gateway (Aug 18 2022 at 14:13): Email Gateway (Aug 18 2022 at 14:13):From: Rick Murphy <rick@rickmurphy.org>
Florian & All:
I've successfully completed my Haskabelle install and just wanted to
validate the syntax produced by Haskabelle. There is one difference from
the example shown in the documentation.
Rather than producing these two lines ...
fun evalExp :: "Exp => int" and
evalBexp :: "Bexp => bool"
My installation of Haskabelle produces these two lines ...
fun evalExp :: "Exp \<Rightarrow> int" and
evalBexp :: "Bexp \<Rightarrow> bool"
Are the lines produced by my installation valid syntax?
The response to the Proof General proof command that executes on that
line is as follows:
Proofs for inductive predicate(s) "evalExp_evalBexp_graph"
Proofs for inductive predicate(s) "evalExp_evalBexp_rel"
constants
evalExp :: "Exp => int"
evalBexp :: "Bexp => bool"
Found termination order: "sum_case size size <mlex> {}"
Email Gateway (Aug 18 2022 at 14:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rick,
Shortly, yes: \<Rightarrow> is an xsymbol synonym for =>.
Hope this helps
Florian
signature.asc
Last updated: Apr 24 2024 at 20:16 UTC