Tests for ExpressionSyntax

Experiments for expressions

axiom GaudisCrypt.Test.a [ProgramSpec] : Lens ℕ State

axiom GaudisCrypt.Test.b [ProgramSpec] : Lens ℕ State

axiom GaudisCrypt.Test.loc [ProgramSpec] : Lens ℕ (ProcedureState Unit)

noncomputable def GaudisCrypt.Test.test [ProgramSpec] : Getter ℕ (ProcedureState Unit)

Equations

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