Compare commits

...

1 Commits

Author SHA1 Message Date
Leonardo de Moura
445745834a chore: remove dead code 2025-05-01 18:09:12 -07:00

View File

@@ -65,19 +65,6 @@ def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
modify fun s => { s with natExprMap := s.natExprMap.insert e x }
return x
private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
(varPrefix : Name) (varType : Expr) (toExpr : α Expr) : GoalM Expr := do
if m.isEmpty then
return e
else
let as := m.toArray
let mut e := e.abstract <| as.map (·.2)
let mut i := as.size
for (p, _) in as.reverse do
e := mkLet (varPrefix.appendIndexAfter i) varType (toExpr p) e
i := i - 1
return e
private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
if h : 0 < vars.size then
RArray.toExpr type id (RArray.ofFn (vars[·]) h)