Re: [isabelle] The environment function



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!

2014-10-15 13:05 GMT-03:00 mahmoud abdelazim <m.abdelazim at 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"
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



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