Email Gateway (Aug 19 2022 at 16:19): Email Gateway (Aug 19 2022 at 16:19):From: mahmoud abdelazim <m.abdelazim@icloud.com>
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” i
the output will for example
“5”
:: "int"
WLG.thy
Email Gateway (Aug 19 2022 at 16:19):From: mahmoud abdelazim <m.abdelazim@icloud.com>
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"
WLG.thy
Email Gateway (Aug 19 2022 at 16:19):From: mahmoud abdelazim <m.abdelazim@icloud.com>
How i can define an “env” function in the theory attached here ,
in such way that if i do the following
value "evalExp (Var 1 ) env”
the output will for example
“5”
:: "int"
WLG.thy
Email Gateway (Aug 19 2022 at 16:19):From: Alfio Martini <alfio.martini@acm.org>
Hi Mahmoud,
Here are some possibilities:
definition state::"nat ⇒ int" where
"state = (λx::nat.0)(3:=5)"
value "evalExp (Var 3) ((λx::nat.0)(3:=(5::int)))"
value "evalExp (Var 3) state"
Hope it helps!
Email Gateway (Aug 19 2022 at 16:21):From: Makarius <makarius@sketis.net>
By using the fun_upd operator in Isabelle/HOL, with its := syntax, e.g.
env(x := 5)
A potential cause of confusion is the re-use of := as notation in your
example. The included version of your WLG.thy avoids that by using bold
versions of concrete syntax everywhere (which might cause other confusion
due to visual similarity with non-bold versions).
Furthermore:
* type names are always lower case, like almost everything else
* datatype constructors are usually capitalized
* CamelCaseIsNotUsedInIsabelle
Makarius
Last updated: Oct 30 2025 at 20:23 UTC