max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove dead functionpreprocessLevels (#4112)

Browse source
This commit is contained in:
Leonardo de Moura 2024-05-08 17:38:04 +02:00 • committed by GitHub
parent 227e861719
commit d7c6920550
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Meta/SynthInstance.lean
View file

@ -664,18 +664,6 @@ private def preprocess (type : Expr) : MetaM Expr :=
let type ← whnf type
mkForallFVars xs type
private def preprocessLevels (us : List Level) : MetaM (List Level × Bool) := do
let mut r := #[]
let mut modified := false
for u in us do
let u ← instantiateLevelMVars u
if u.hasMVar then
r := r.push (← mkFreshLevelMVar)
modified := true
else
r := r.push u
return (r.toList, modified)
private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (outParamsPos : Array Nat) : MetaM (Array Expr) := do
if h : i < args.size then
let type ← whnf type