[isabelle] haskabelle syntax check



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*> {}"

--
Rick

cell: 703-201-9129
web:  http://www.rickmurphy.org
blog: http://phaneron.rickmurphy.org





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