Hello,
I am very new to Coq.
As part of a project, I need to create denotational semantics and test it with Coq.
I’m trying to transform a piece of code into Coq but I don’t know how!
Below is the part of the sematics and my test in Coq:
Definition assignment (var:Exp)( e:Exp) (rhoF :Envf )(rho:Env )(s:State)(Ks :Cs): mSStm :=
let (K0e : Ce) := (v0 , s0) => Ks((rho var) → v0)
in let (v1,s1) := mExp e rhoF rho s K0e
in s1 .
Thanks