[isabelle] expression evaluation

Hi all,

I have a question about evaluation of expression.

I would like to define the following function:

     eval_expr : expr => (mess +  {err} )

which evaluate an expression "expr", otherwise returns an error message "err".
"expr" and "mess" are declared as nominal_datatype.

Any clues?


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