Documentation

Lean.Elab.Config

Equations
  • Lean.Elab.Term.setElabConfig cfg = { foApprox := true, ctxApprox := true, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := cfg.isDefEqStuckEx, transparency := cfg.transparency, zetaNonDep := cfg.zetaNonDep, trackZeta := cfg.trackZeta, unificationHints := cfg.unificationHints, proofIrrelevance := cfg.proofIrrelevance, assignSyntheticOpaque := cfg.assignSyntheticOpaque, ignoreLevelMVarDepth := cfg.ignoreLevelMVarDepth, offsetCnstrs := cfg.offsetCnstrs, etaStruct := cfg.etaStruct }