update

Author: Koukyosyumei

Loda/Env.lean

@@ -79,7 +79,7 @@ def getCircuitFromEnv (name : String) : Lean.CoreM (Option Ast.Circuit) := do
   return lookupCircuit (circuitExt.getState env) name
 
 /-- A type environment: maps variable names to Loda `Ty`s. -/
-def TyEnv := List (String × Ast.Ty)
+abbrev TyEnv := List (String × Ast.Ty)
 
 /--
   Extend `Γ` by binding `ident` to `τ`.

Loda/PropSemantics.lean

@@ -53,7 +53,7 @@ match Env.lookupTy Γ ident, Env.lookupVal σ ident with
 -- any other case is false
 | _, _ => False
 
-def tyenvToProp (σ: Env.ValEnv) (Δ: Env.CircuitEnv) (Γ: List (String × Ast.Ty)): Prop :=
+def tyenvToProp (σ: Env.ValEnv) (Δ: Env.CircuitEnv) (Γ: Env.TyEnv): Prop :=
   ∀ e ∈ Γ, varToProp σ Δ Γ e.1
 
 end PropSemantics

Loda/Typing.lean

@@ -158,13 +158,7 @@ def circuitCorrect (δ : Env.CircuitEnv) (c : Ast.Circuit) : Prop :=
     PropSemantics.tyenvToProp σ δ Γ →
     @TypeJudgment σ δ Γ c.body c.output.snd
 
-/-
-  (hΓx : Env.lookupTy Γ x = Ty.refin Ty.field (Predicate.eq ex))
-  (htyenv: PropSemantics.tyenvToProp σ Δ Γ x)
-  (hmt : PropSemantics.multi_tyenvToProp σ Δ Γ)
--/
-
-lemma lookupTy_mem (Γ: List (String × Ast.Ty)) (x: String) (τ :Ast.Ty) (φ: Ast.Predicate)
+lemma lookupTy_mem (Γ: Env.TyEnv) (x: String) (τ :Ast.Ty) (φ: Ast.Predicate)
   (h : Env.lookupTy Γ x = Ast.Ty.refin τ φ) :
   (x, Ast.Ty.refin τ φ) ∈ Γ := by
   by_contra hn
@@ -179,7 +173,7 @@ lemma lookupTy_mem (Γ: List (String × Ast.Ty)) (x: String) (τ :Ast.Ty) (φ: A
   }
 
 lemma tyenvToProp_implies_varToProp
-  (σ : Env.ValEnv) (Δ : Env.CircuitEnv) (Γ : List (String × Ast.Ty))
+  (σ : Env.ValEnv) (Δ : Env.CircuitEnv) (Γ : Env.TyEnv)
   (x : String) (τ : Ast.Ty) (φ : Ast.Predicate)
   (hΓx : Env.lookupTy Γ x = Ast.Ty.refin τ φ)
   (hmt : PropSemantics.tyenvToProp σ Δ Γ) :