def DocGen4.Process.getInstanceTypes (typ : Lean.Expr) : Lean.MetaM (Array Lean.Name)

Equations

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

def DocGen4.Process.getInstanceTypes.findName : Lean.BinderInfo × Lean.Expr → StateRefT' IO.RealWorld (Array Lean.Name) Lean.MetaM Unit

Equations

• DocGen4.Process.getInstanceTypes.findName (Lean.BinderInfo.default, Lean.Expr.sort Lean.Level.zero) = modify fun (x : Array Lean.Name) => x.push `_builtin_prop
• DocGen4.Process.getInstanceTypes.findName (Lean.BinderInfo.default, Lean.Expr.sort a.succ) = modify fun (x : Array Lean.Name) => x.push `_builtin_typeu
• DocGen4.Process.getInstanceTypes.findName (Lean.BinderInfo.default, Lean.Expr.sort u) = modify fun (x : Array Lean.Name) => x.push `_builtin_sortu
• DocGen4.Process.getInstanceTypes.findName (Lean.BinderInfo.default, e) = match e.getAppFn with | Lean.Expr.const name us => modify fun (x : Array Lean.Name) => x.push name | x => pure ()
• DocGen4.Process.getInstanceTypes.findName a✝ = pure ()

def DocGen4.Process.getInstPriority (name : Lean.Name) : Lean.MetaM (Option Nat)

Equations

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

def DocGen4.Process.InstanceInfo.ofDefinitionVal (v : Lean.DefinitionVal) : AnalyzeM InstanceInfo

Equations

• DocGen4.Process.InstanceInfo.ofDefinitionVal v = do let info ← DocGen4.Process.DefinitionInfo.ofDefinitionVal v liftM (DocGen4.Process.InstanceInfo.ofDefinitionInfo✝ info v.type)

def DocGen4.Process.InstanceInfo.ofTheoremVal (v : Lean.TheoremVal) : Lean.MetaM InstanceInfo

Equations

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