[isabelle] The environment function




How i can define an “env” function in the theory attached here ,
in such way that if i do the following
value "evalExp (Var x ) env” 

the output will for example
“5”
:: "int"

Attachment: WLG.thy
Description: Binary data



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