def Assignment01.I {α : Sort u_1} : α → α

Equations

• Assignment01.I a = a

def Assignment01.K {α : Sort u_1} {β : Sort u_2} : α → β → α

Equations

• Assignment01.K a x✝ = a

def Assignment01.C {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} : (α → β → γ) → β → α → γ

Equations

• Assignment01.C f a b = f b a

def Assignment01.projFst {α : Sort u_1} : α → α → α

Equations

• Assignment01.projFst a x✝ = a

def Assignment01.projSnd {α : Sort u_1} : α → α → α

Equations

• Assignment01.projSnd x✝ b = b

def Assignment01.someNonsense {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} : (α → β → γ) → α → (α → γ) → β → γ

Equations

• Assignment01.someNonsense f a x✝ b = f a b

structure Assignment01.RectangularPrism : Type

• height : Float
• width : Float
• depth : Float

def Assignment01.instReprRectangularPrism.repr : RectangularPrism → Nat → Std.Format

Equations

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

instance Assignment01.instReprRectangularPrism : Repr RectangularPrism

Equations

• Assignment01.instReprRectangularPrism = { reprPrec := Assignment01.instReprRectangularPrism.repr }

def Assignment01.volume (r : RectangularPrism) : Float

Equations

• Assignment01.volume r = r.height * r.width * r.depth

structure Assignment01.Point : Type

• x : Float
• y : Float

instance Assignment01.instReprPoint : Repr Point

Equations

• Assignment01.instReprPoint = { reprPrec := Assignment01.instReprPoint.repr }

def Assignment01.instReprPoint.repr : Point → Nat → Std.Format

Equations

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

structure Assignment01.Segment : Type

• p1 : Point
• p2 : Point

def Assignment01.instReprSegment.repr : Segment → Nat → Std.Format

Equations

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

instance Assignment01.instReprSegment : Repr Segment

Equations

• Assignment01.instReprSegment = { reprPrec := Assignment01.instReprSegment.repr }

def Assignment01.length (s : Segment) : Float

Equations

• Assignment01.length s = ((s.p2.x - s.p1.x) * (s.p2.x - s.p1.x) + (s.p2.y - s.p1.y) * (s.p2.y - s.p1.y)).sqrt

def Assignment01.Names1 : List String

Equations

• Assignment01.Names1 = ["RectangularPrism.mk", "RectangularPrism.height", "RectangularPrism.width", "RectangularPrism.depth"]

structure Assignment01.Hamster : Type

• name : String
• fluffy : Bool

structure Assignment01.Book : Type

• makeBook :: (
• title : String
• author : String
• price : Float
• )

def Assignment01.Names2 : List String

Equations

• Assignment01.Names2 = ["Hamster.mk", "Hamster.name", "Hamster.fluffy", "Book.makeBook", "Book.title", "Book.author", "Book.price"]

def Assignment01.product (ns : List Nat) : Nat

Equations

• Assignment01.product [] = 1
• Assignment01.product (n :: ns_2) = n * Assignment01.product ns_2