Tests for ExpressionSyntax

Experiments for expressions

axiom GaudisCrypt.Test.a : Lens ℕ VariableAssignment

axiom GaudisCrypt.Test.b : Lens ℕ VariableAssignment

axiom GaudisCrypt.Test.loc : Lens ℕ ProgramState

noncomputable def GaudisCrypt.Test.test : Getter ℕ ProgramState

Equations

• GaudisCrypt.Test.test = { get := fun (st : GaudisCrypt.ProgramState) => §GaudisCrypt.Test.a + §GaudisCrypt.Test.loc }