From 4506f7c2424d229c4f919b339525afa2cbcebb33 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 08:56:31 -0500 Subject: [PATCH] Delete dead code from Base.lean Signed-off-by: Danila Fedorin --- lean/Spa/Language/Base.lean | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean index 1228cc3..78e68b7 100644 --- a/lean/Spa/Language/Base.lean +++ b/lean/Spa/Language/Base.lean @@ -21,17 +21,6 @@ inductive Stmt where | whileLoop (e : Expr) (s : Stmt) deriving DecidableEq -inductive Expr.HasVar : String → Expr → Prop - | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂) - | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂) - | subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂) - | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂) - | here {k} : Expr.HasVar k (.var k) - -inductive BasicStmt.HasVar : String → BasicStmt → Prop - | assignLeft {k e} : BasicStmt.HasVar k (.assign k e) - | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e) - def Expr.vars : Expr → Finset String | .add l r => l.vars ∪ r.vars | .sub l r => l.vars ∪ r.vars @@ -48,7 +37,4 @@ def Stmt.vars : Stmt → Finset String | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars | .whileLoop e s => e.vars ∪ s.vars -def Stmt.varsList (ss : List Stmt) : Finset String := - ss.foldr (fun s acc => s.vars ∪ acc) ∅ - end Spa