Documentation

Lean.PrettyPrinter.Delaborator.TopDownAnalyze

Equations
Equations
Equations
Equations
Equations
Equations
  • Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning t s = withReader (fun ctx => { config := let src := ctx.config; { foApprox := src.foApprox, ctxApprox := src.ctxApprox, quasiPatternApprox := src.quasiPatternApprox, constApprox := src.constApprox, isDefEqStuckEx := src.isDefEqStuckEx, transparency := src.transparency, zetaNonDep := src.zetaNonDep, trackZeta := src.trackZeta, unificationHints := src.unificationHints, proofIrrelevance := src.proofIrrelevance, assignSyntheticOpaque := true, ignoreLevelMVarDepth := src.ignoreLevelMVarDepth, offsetCnstrs := src.offsetCnstrs, etaStruct := src.etaStruct }, lctx := ctx.lctx, localInstances := ctx.localInstances, defEqCtx? := ctx.defEqCtx?, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }) (Lean.Meta.isDefEq t s)
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations