Lean4
def findType (t : Expr) : TermElabM Unit :=
withReducible do
let t ← instantiateMVars t
let head := (← forallMetaTelescopeReducing t).2.2.toHeadIndex
let pat ← abstractMVars t
let env ← getEnv
let mut numFound := 0
for n in (← findDeclsPerHead.get).getD head #[]do
let c := env.find? n |>.get!
let cTy := c.instantiateTypeLevelParams (← mkFreshLevelMVars c.numLevelParams)
let found ←
forallTelescopeReducing cTy fun cParams cTy' ↦ do
let pat := pat.expr.instantiateLevelParamsArray pat.paramNames (← mkFreshLevelMVars pat.numMVars).toArray
let (_, _, pat) ← lambdaMetaTelescope pat
let (patParams, _, pat) ← forallMetaTelescopeReducing pat
isDefEq cTy' pat <&&> matchHyps patParams.toList [] cParams.toList
if found then
numFound := numFound + 1
if numFound > 20 then
logInfo m!"maximum number of search results reached"
break
logInfo m! "{n }: {cTy}"
