chore: remove dead code (#8197)
This commit is contained in:
parent
af4c693030
commit
1143b4766c
1 changed files with 0 additions and 13 deletions
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue