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
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
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
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!
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: Nov 21 2024 at 12:39 UTC