Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] expression evaluation

view this post on Zulip Email Gateway (Aug 18 2022 at 10:05):

From: Temesghen Kahsai <lememta@gmail.com>
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?

Thanks.

Last updated: Nov 21 2024 at 12:39 UTC