← Copula mathematical handbook

def LeanServerTestRefsTest0 : Type

Equations

• LeanServerTestRefsTest0 = Nat

def Lean.Server.Test.LeanServerTestRefsTest0' : Type

Equations

• Lean.Server.Test.LeanServerTestRefsTest0' = Nat

def Lean.Server.Test.Refs.Test1 : Type

Equations

• Lean.Server.Test.Refs.Test1 = Nat

def Lean.Server.Test.Refs.Test2 : Type

Equations

• Lean.Server.Test.Refs.Test2 = Lean.Server.Test.Refs.Test1

def Lean.Server.Test.Refs.Test3 : Type

Equations

• Lean.Server.Test.Refs.Test3 = Lean.Server.Test.Refs.Test1

def Lean.Server.Test.Refs.Test4 : Type

Equations

• Lean.Server.Test.Refs.Test4 = Lean.Server.Test.Refs.Test2

def Lean.Server.Test.Refs.Test5 : Type

Equations

• Lean.Server.Test.Refs.Test5 = Lean.Server.Test.Refs.Test2

inductive Lean.Server.Test.Refs.Test6 : Type

• mk : Test6

def Lean.Server.Test.Refs.test7 : Test6

Equations

• Lean.Server.Test.Refs.test7 = Lean.Server.Test.Refs.Test6.mk

def Lean.Server.Test.Refs.test8 : Test6

Equations

• Lean.Server.Test.Refs.test8 = Lean.Server.Test.Refs.Test6.mk

def Lean.Server.Test.Refs.test9 : Test6

Equations

• Lean.Server.Test.Refs.test9 = Lean.Server.Test.Refs.test7

def Lean.Server.Test.Refs.test10 : Test6

Equations

• Lean.Server.Test.Refs.test10 = Lean.Server.Test.Refs.test9