[isabelle] Is Simpl code executable?



Hi all,

I'm wondering if anyone knows whether Simpl code is executable.
I am new at using Simpl and noticed that I can express
things that I cannot express in other imperative languages.
For example, assigning variables to functions defined in
isabelle (which are in general not necessarily even computable)
or setting the conditions of while loops or if statements to
boolean expressions starting with "exists or forall".

I'm wondering how one can be sure that the Simpl code they
write is executable (without automatically parsing it from an
imperative language like C).

Best,
Christine




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