def DUnif.metaEta (e : Lean.Expr) : Lean.MetaM (Option Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.

def DUnif.metaEta.metaEtaAux (e : Lean.Expr) : Lean.MetaM (Option (Lean.MVarId × Lean.Expr × Array Nat))

Equations

• One or more equations did not get rendered due to their size.

def DUnif.mkGeneralFnTy (n : Nat) (resTy : Option Lean.Expr := none) : Lean.MetaM Lean.Expr

Make the most general function type with n explicit binders

Equations

• One or more equations did not get rendered due to their size.
• DUnif.mkGeneralFnTy 0 (some resTy_2) = pure resTy_2
• DUnif.mkGeneralFnTy 0 = Lean.Meta.mkFreshTypeMVar

def DUnif.mkImplication (n : Nat) (resTy : Option Lean.Expr := none) : Lean.MetaM Lean.Expr

Make an implication with n explicit binders

Equations

• One or more equations did not get rendered due to their size.