structure Half (n : ℕ) : Type

• val : ℕ
• isHalf : self.val + self.val = n

instance instReprHalf {n✝ : ℕ} : Repr (Half n✝)

Equations

• instReprHalf = { reprPrec := reprHalf✝ }

def half? (n : ℕ) : Option (Half n)

Equations

• half? 0 = some { val := 0, isHalf := half?.proof_3 }
• half? 1 = none
• half? k.succ.succ = Option.map (fun (x : Half k) => match x with | { val := m, isHalf := p } => { val := m + 1, isHalf := ⋯ }) (half? k)

Option is a monad. We can use do notation to simplify the code.

def OneAndAHalf (n : ℕ) : Option ℕ

Equations

• OneAndAHalf n = do let __discr ← half? n match __discr with | { val := m, isHalf := isHalf } => pure (3 * m)

def quarter (n : ℕ) : Option ℕ

Equations

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

def quarterWithProof (n : ℕ) : Option { k : ℕ // k + k + k + k = n }

Equations

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

def half?' (n? : Option ℕ) : Option ℕ

Equations

• half?' n? = do let n ← n? let __discr ← half? n match __discr with | { val := m, isHalf := isHalf } => pure m

def half! (n : ℕ) : ℕ

Equations

• half! 0 = 0
• half! 1 = panicWithPosWithDecl "PfsProgs25.Unit10.Half" "half!" 81 9 "odd number"
• half! k.succ.succ = half! k + 1