6. Poly: Polymorphism and Higher-Order Functions🔗

import LF.Induction
import LF.UsingLean

6.1. Polymorphism🔗

6.1.1. Polymorphic Lists🔗

Instead of defining new lists for each type, like this...

inductive BoolList : Type where
  | nil
  | cons (b : Bool) (l : BoolList)

... Lean lets us give a polymorphic definition that allows list elements of any type:

inductive MyList (α : Type) : Type where
  | nil : MyList α
  | cons (x : α) (l : MyList α) : MyList α

We can now write MyList Nat in place of a specialized list-of-numbers type.

What is MyList itself?

It is a type constructor — a function from Types to Types.

Note to developers (Yipeng Liu @berberman)

A trick used below: parenthesizing the declaration makes it a term — Lean elaborates it and prints its inferred function type, instead of the declaration signature: MyList (α : Type) : Type.

MyList : Type → Type#check (MyList)

MyList : Type → Type

The α in the definition of MyList becomes an implicit parameter to the list constructors nil and cons.

MyList.nil {α : Type} : MyList α#check MyList.nil

MyList.nil {α : Type} : MyList α

MyList.cons 3 MyList.nil : MyList Nat#check MyList.cons 3 MyList.nil

MyList.cons 3 MyList.nil : MyList Nat

MyList.nil {α : Type} : MyList α#check MyList.nil

MyList.nil {α : Type} : MyList α

MyList.cons {α : Type} (x : α) (l : MyList α) : MyList α#check MyList.cons

MyList.cons {α : Type} (x : α) (l : MyList α) : MyList α

We can now define polymorphic versions of the functions we've already seen...

def replicate (α : Type) (x : α) (count : Nat) : MyList α :=
  match count with
  | 0 => .nil
  | count' + 1 => .cons x (replicate α x count')

Some simple facts about replicate:

theorem replicate_zero (α : Type) (a : α) :
    replicate α a 0 = MyList.nil := rfl

theorem replicate_succ (α : Type) (a : α) (count : Nat) :
    replicate α a (count + 1) = MyList.cons a (replicate α a count) := rfl

example : replicate Nat 4 2 = .cons 4 (.cons 4 .nil) := byα:Typeβ:Typeγ:Typex:αy:β⊢ replicate Nat 4 2 = MyList.cons 4 (MyList.cons 4 MyList.nil) rflAll goals completed! 🐙

example : replicate Bool false 1 = .cons false .nil := byα:Typeβ:Typeγ:Typex:αy:β⊢ replicate Bool false 1 = MyList.cons false MyList.nil rflAll goals completed! 🐙

Quiz

What is the type of MyList.cons true (MyList.cons 3 MyList.nil)?

(A) MyList Nat

(B) {α : Type} → α → MyList α → MyList α

(D) MyList (Nat × Bool)

(E) Ill-typed

Show solution

(E)

Quiz

What is the type of replicate?

(A) Nat → Nat → MyList Nat

(B) (α : Type) → α → Nat → MyList α

(D) Ill-typed

Show solution

(B)

Quiz

What is the type of replicate 1 2?

(A) MyList Nat

(B) (α : Type) → α → Nat → MyList α

(D) Ill-typed

Show solution

(D)

From now on we'll use Lean's built-in List α type with notations [], ::, [1, 2, 3], and ++.

example : List Nat := [1, 2, 3]

6.1.1.1. Implicit Type Arguments and Argument Synthesis🔗

Supplying every type argument is also boring, but Lean can usually infer them:

def replicate' (α : Type) (x : α) (count : Nat) : List α :=
  match count with
  | 0 => []
  | count' + 1 => x :: replicate' _ x count'

Alternatively, we can declare arguments implicit by surrounding them with curly braces instead of parens:

def replicate'' {α : Type} (x : α) (count : Nat) : List α :=
  match count with
  | 0 => []
  | count' + 1 => x :: replicate'' x count'

6.1.1.2. Supplying Type Arguments Explicitly🔗

In general, it's fine to just let Lean infer all type arguments. But occasionally this can lead to problems:

def Failed to infer type of definition `mynil`mynil := don't know how to synthesize implicit argument `α`
  @List.nil ?m.3
context:
α β γ:Typex:αy:β⊢ Type u_1[]

Failed to infer type of definition `mynil`

We can fix this with an explicit type annotation.

We use the @ prefix when we want to supply the type argument explicitly. The @ makes all implicit arguments of a function explicit:

@List.nil : {α : Type u_1} → List α#check @List.nil

def myNil' := @List.nil Nat

@List.nil : {α : Type u_1} → List α

Quiz

Which type does Lean assign to the following expression? (The square brackets in this quiz and the following ones are list brackets.)

[1, 2, 3]

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(A)

Quiz

What about this one?

[3 + 4] ++ []

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(A)

Quiz

What about this one?

(true && false) :: []

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(B)

Quiz

What about this one?

[1, []]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(D)

Quiz

What about this one?

[[1], []]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(B)

Quiz

And what about this one?

[1] :: [[]]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(B)

Quiz

This one?

@List.nil Bool

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(C)

6.1.1.3. Exercises🔗

def List.rev {α : Type} (l : List α) : List α :=
  match l with
  | .nil => .nil
  | .cons h t => rev t ++ (.cons h .nil)

theorem rev_nil {α : Type} : ([] : List α).rev = [] := byα:Type⊢ [].rev = [] rflAll goals completed! 🐙

theorem rev_cons {α : Type} {x : α} {l : List α} :
    (x :: l).rev = l.rev ++ [x] := byα:Typex:αl:List α⊢ (x :: l).rev = l.rev ++ [x] rflAll goals completed! 🐙

Exercise★★(poly_exercises)

Here are a few simple exercises, just like ones in the Lists chapter, for practice with polymorphism. Complete the proofs below. You will find the following characterizing lemmas for List.append in Lean standard library to be useful:

List.nil_append.{u} {α : Type u} (as : List α) : [] ++ as = as#check List.nil_append
List.cons_append.{u} {α : Type u} {a : α} {as bs : List α} : a :: as ++ bs = a :: (as ++ bs)#check List.cons_append

List.cons_append.{u} {α : Type u} {a : α} {as bs : List α} : a :: as ++ bs = a :: (as ++ bs)

List.nil_append.{u} {α : Type u} (as : List α) : [] ++ as = as

theorem declaration uses `sorry`append_nil {α : Type} {l : List α} :
    l ++ [] = l := byα:Typel:List α⊢ l ++ [] = l
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`append_assoc {α : Type} {l₁ l₂ l₃ : List α} :
    l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃) := byα:Typel₁:List αl₂:List αl₃:List α⊢ l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃)
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`append_length {α : Type} {l₁ l₂ : List α} :
    (l₁ ++ l₂).length = l₁.length + l₂.length := byα:Typel₁:List αl₂:List α⊢ (l₁ ++ l₂).length = l₁.length + l₂.length
  sorryAll goals completed! 🐙

Exercise★★(more_poly_exercises)

Here are some slightly more interesting ones...

theorem declaration uses `sorry`reverse_append {α : Type} {l₁ l₂ : List α} :
    (l₁ ++ l₂).rev = l₂.rev ++ l₁.rev := byα:Typel₁:List αl₂:List α⊢ (l₁ ++ l₂).rev = l₂.rev ++ l₁.rev
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`reverse_reverse {α : Type} (l : List α) :
    l.rev.rev = l := byα:Typel:List α⊢ l.rev.rev = l
  sorryAll goals completed! 🐙

6.1.2. Polymorphic Pairs🔗

Like inductives, structures can also be made polymorphic. If we generalize the definition NatProd of pairs of natural numbers from last chapter, we get polymorphic pairs, often called products:

structure MyProd (α β : Type) where
  fst : α
  snd : β

Lean's built-in product type Prod provides a Prod.mk constructor, and Prod.fst and Prod.snd functions for accessing the first and second components of the pair. It also has special syntax for creating products:

(1, true) : Nat × Bool#check (1, true)
1#eval (1, true).fst
true#eval (1, true).snd

(1, true) : Nat × Bool

true

You can also use .1 instead of .fst and .2 instead of .snd:

example : (3, 5).1 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ (3, 5).fst = 3 rflAll goals completed! 🐙
example : (3, 5).2 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ (3, 5).snd = 5 rflAll goals completed! 🐙

Lean writes the product type Prod α β as α × β. In VS Code you can type \times or \x to enter the × symbol.

The dsimp only tactic can be used to simplify (x, y).fst into x and (x, y).snd into y.

Be careful not to get (x, y) and α × β confused!

What does this function do?

def zip {α β : Type} (l₁ : List α) (l₂ : List β) : List (α × β) :=
  match l₁, l₂ with
  | [], [] => []
  | _ :: _, [] => []
  | [], _ :: _ => []
  | x :: l₁', y :: l₂' => (x, y) :: zip l₁' l₂'

theorem zip_nil_left {α β : Type} (l₁ : List α) : zip l₁ [] = ([] : List (α × β)) := byα:Typeβ:Typel₁:List α⊢ zip l₁ [] = []
  cases l₁nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:αtail✝:List α⊢ zip (head✝ :: tail✝) [] = [] <;>nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:αtail✝:List α⊢ zip (head✝ :: tail✝) [] = [] rflAll goals completed! 🐙

theorem zip_nil_right {α β : Type} (l₂ : List β) : zip [] l₂ = ([] : List (α × β)) := byα:Typeβ:Typel₂:List β⊢ zip [] l₂ = []
  cases l₂nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:βtail✝:List β⊢ zip [] (head✝ :: tail✝) = [] <;>nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:βtail✝:List β⊢ zip [] (head✝ :: tail✝) = [] rflAll goals completed! 🐙

theorem zip_cons_cons {α β : Type} {x : α} {y : β} {l₁ : List α} {l₂ : List β} :
   zip (x :: l₁) (y :: l₂) = (x, y) :: zip l₁ l₂ := byα:Typeβ:Typex:αy:βl₁:List αl₂:List β⊢ zip (x :: l₁) (y :: l₂) = (x, y) :: zip l₁ l₂ rflAll goals completed! 🐙

Notice that the simplification lemmas zip_nil_left and zip_nil_right are not proofs by rfl. The reason is that l₁ and l₂ are variables, and matching on a variable usually gets stuck, like we have seen before in Induction when proving the zero_add theorem. To overcome this, we destruct the list so that the match knows which branch to take during the computation done by the rfl tactic.

6.1.3. Polymorphic Options🔗

def nth? {α : Type} (l : List α) (n : Nat) : Option α :=
  match l with
  | [] => none
  | x :: l' => match n with
    | 0 => some x
    | n' + 1 => nth? l' n'

theorem nth?_nil {α : Type} {n : Nat} :
  nth? ([] : List α) n = none := byα:Typen:Nat⊢ nth? [] n = none rflAll goals completed! 🐙

theorem nth?_cons_zero {α : Type} {x : α} {l' : List α} :
  nth? (x :: l') 0 = some x := byα:Typex:αl':List α⊢ nth? (x :: l') 0 = some x rflAll goals completed! 🐙

theorem nth?_cons_succ {α : Type} {x : α} {l' : List α} {n : Nat} :
  nth? (x :: l') (n + 1) = nth? l' n := byα:Typex:αl':List αn:Nat⊢ nth? (x :: l') (n + 1) = nth? l' n rflAll goals completed! 🐙

example : nth? [4, 5, 6, 7] 0 = some 4 := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [4, 5, 6, 7] 0 = some 4 rflAll goals completed! 🐙
example : nth? [[1], [2]] 1 = some [2] := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [[1], [2]] 1 = some [2] rflAll goals completed! 🐙
example : nth? [true] 2 = none := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [true] 2 = none rflAll goals completed! 🐙

6.2. Functions as Data🔗

6.2.1. Higher-Order Functions🔗

Functions that take other functions as arguments or return them as results are called higher-order functions.

def doIt3Times {α : Type} (f : α → α) (x : α) : α :=
  f (f (f x))

doIt3Times {α : Type} (f : α → α) (x : α) : α#check doIt3Times

example : doIt3Times Nat.minusTwo 9 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times Nat.minusTwo 9 = 3 rflAll goals completed! 🐙

example : doIt3Times not true = false := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times not true = false rflAll goals completed! 🐙

doIt3Times {α : Type} (f : α → α) (x : α) : α

6.2.2. Filter🔗

A higher-order function can take another function as an argument. For example, filter takes a test and a list.

def filter {α : Type} (test : α → Bool) (l : List α) : List α :=
  match l with
  | [] => []
  | x :: l' =>
    bif test x then x :: filter test l'
    else filter test l'

example : filter Nat.even [1, 2, 3, 4] = [2, 4] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter Nat.even [1, 2, 3, 4] = [2, 4] rflAll goals completed! 🐙

Here are some further examples and properties of filter.

def isLength1 {α : Type} (l : List α) : Bool :=
  l.length == 1

example : filter isLength1
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter isLength1 [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

theorem filter_nil {α : Type} {test : α → Bool} :
  filter test [] = [] := byα:Typetest:α → Bool⊢ filter test [] = [] rflAll goals completed! 🐙

theorem filter_cons_of_pos {α : Type} {test : α → Bool} {x : α}
    {l : List α} (h : test x = true) :
    filter test (x :: l) = x :: filter test l := byα:Typetest:α → Boolx:αl:List αh:test x = true⊢ filter test (x :: l) = x :: filter test l
  rw [filter,α:Typetest:α → Boolx:αl:List αh:test x = true⊢ (bif test x then x :: filter test l else filter test l) = x :: filter test l h,α:Typetest:α → Boolx:αl:List αh:test x = true⊢ (bif true then x :: filter test l else filter test l) = x :: filter test l Bool.cond_trueα:Typetest:α → Boolx:αl:List αh:test x = true⊢ x :: filter test l = x :: filter test l]All goals completed! 🐙

theorem filter_cons_of_neg {α : Type} {test : α → Bool} {x : α}
    {l : List α} (h : test x = false) :
    filter test (x :: l) = filter test l := byα:Typetest:α → Boolx:αl:List αh:test x = false⊢ filter test (x :: l) = filter test l
   rw [filter,α:Typetest:α → Boolx:αl:List αh:test x = false⊢ (bif test x then x :: filter test l else filter test l) = filter test l h,α:Typetest:α → Boolx:αl:List αh:test x = false⊢ (bif false then x :: filter test l else filter test l) = filter test l Bool.cond_falseα:Typetest:α → Boolx:αl:List αh:test x = false⊢ filter test l = filter test l]All goals completed! 🐙

Note that x and l are implicit too, following a general convention: any argument an equation's shape determines when applied is made implicit, so using rw lemmas requires no extra _ arguments.

The filter function (especially when combined with some other functions we'll see later) enables a powerful wholemeal (or collection-oriented) programming style.

def countOddMembers (l : List Nat) : Nat := (filter Nat.odd l).length

example : countOddMembers [1, 0, 3, 1, 4, 5] = 4 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [1, 0, 3, 1, 4, 5] = 4 rflAll goals completed! 🐙
example : countOddMembers [0, 2, 4] = 0 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [0, 2, 4] = 0 rflAll goals completed! 🐙
example : countOddMembers [] = 0 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [] = 0 rflAll goals completed! 🐙

6.2.3. Anonymous Functions🔗

Functions can be constructed "on the fly" without giving them names.

example : doIt3Times (fun n => n * n) 2 = 256 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (fun n => n * n) 2 = 256 rflAll goals completed! 🐙

Lean also provides the shorter · notation for anonymous functions.

example : doIt3Times (· + 1) 0 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (fun x => x + 1) 0 = 3 rflAll goals completed! 🐙

example : filter (fun l => l.length == 1)
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter (fun l => l.length == 1) [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

example : filter (·.length == 1)
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter (fun x => x.length == 1) [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

6.2.4. Map🔗

def map {α β : Type} (f : α → β) (l : List α) : List β :=
  match l with
  | [] => []
  | head :: tail => f head :: map f tail

example : map (· + 3) [2, 0, 2] = [5, 3, 5] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map (fun x => x + 3) [2, 0, 2] = [5, 3, 5] rflAll goals completed! 🐙

example : map Nat.odd [2, 1, 2, 5] = [false, true, false, true] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map Nat.odd [2, 1, 2, 5] = [false, true, false, true] rflAll goals completed! 🐙

example : map (fun n => [n.even, n.odd]) [2, 1, 2, 5]
  = [[true, false], [false, true], [true, false], [false, true]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map (fun n => [n.even, n.odd]) [2, 1, 2, 5] = [[true, false], [false, true], [true, false], [false, true]] rflAll goals completed! 🐙

Quiz

Recall the definition of map:

def map {α β : Type} (f : α → β) (l : List α) : List β :=
  match l with
  | [] => []
  | head :: tail => f head :: map f tail

What is the type of @map?

(A) {α β : Type} → α → β → List α → List β

(B) α → β → List α → List β

(D) {α : Type} → (α → α) → List α → List α

As usual, we define the following simplification rules for map:

theorem map_nil {α : Type} {β : Type} {f : α → β} : map f [] = [] := byα:Typeβ:Typef:α → β⊢ map f [] = [] rflAll goals completed! 🐙

theorem map_cons {α : Type} {β : Type} {f : α → β} {x : α} {l : List α} :
    map f (x :: l) = f x :: map f l := byα:Typeβ:Typef:α → βx:αl:List α⊢ map f (x :: l) = f x :: map f l rflAll goals completed! 🐙

Lists are not the only inductive type for which map makes sense. Here is a map for the Option type:

def optionMap {α : Type} {β : Type} (f : α → β) (x? : Option α) : Option β :=
  match x? with
  | none => none
  | some x => some (f x)

6.2.5. Fold🔗

def fold {α : Type} {β : Type} (f : α → β → β) (l : List α) (b : β) : β :=
  match l with
  | [] => b
  | a :: l => f a (fold f l b)

This is the "reduce" in map/reduce...

example : fold (· && ·) [true, true, false, true] true = false := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 && x2) [true, true, false, true] true = false rflAll goals completed! 🐙

example : fold (· * ·) [1, 2, 3, 4] 1 = 24 := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 * x2) [1, 2, 3, 4] 1 = 24 rflAll goals completed! 🐙

example : fold (· ++ ·) [[1], [], [2, 3], [4]] [] = [1, 2, 3, 4] := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 ++ x2) [[1], [], [2, 3], [4]] [] = [1, 2, 3, 4] rflAll goals completed! 🐙

example : fold (fun l n => l.length + n) [[1], [], [2, 3, 2], [4]] 0 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun l n => l.length + n) [[1], [], [2, 3, 2], [4]] 0 = 5 rflAll goals completed! 🐙

theorem fold_nil {α β : Type} {f : α → β → β} {b : β} :
  fold f [] b = b := byα:Typeβ:Typef:α → β → βb:β⊢ fold f [] b = b rflAll goals completed! 🐙

theorem fold_cons {α β : Type} {f : α → β → β} {a : α} {l : List α} {b : β} :
  fold f (a :: l) b = f a (fold f l b) := byα:Typeβ:Typef:α → β → βa:αl:List αb:β⊢ fold f (a :: l) b = f a (fold f l b) rflAll goals completed! 🐙

Quiz

Here is the definition of fold again:

def fold {α β : Type} (f : α → β → β) (l : List α) (b : β) : β :=
  match l with
  | [] => b
  | a :: l => f a (fold f l b)

What is the type of @fold?

(A) {α β : Type} → (α → β → β) → List α → β → β

(B) α → β → (α → β → β) → List α → β → β

(D) α → β → α → β → β → List α → β → β

Show solution

(A)

Quiz

What does fold (· + ·) [1, 2, 3, 4] 0 simplify to?

(A) [1, 2, 3, 4]

(B) 0

(D) [3, 7, 0]

Show solution

(C)

6.2.6. Functions That Construct Functions🔗

Here are two functions that return functions as results.

def constFun {α : Type} (x : α) : Nat → α :=
  fun _ => x

def fTrue := constFun true

example : fTrue 0 = true := byα:Typeβ:Typeγ:Typex:αy:β⊢ fTrue 0 = true rflAll goals completed! 🐙

example : constFun 5 99 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ constFun 5 99 = 5 rflAll goals completed! 🐙

A two-argument function in Lean is actually a function that returns a function!

Nat.add : Nat → Nat → Nat#check Nat.add

Nat.add : Nat → Nat → Nat

def plus3 := Nat.add 3
plus3 : Nat → Nat#check plus3

example : plus3 4 = 7 := byα:Typeβ:Typeγ:Typex:αy:β⊢ plus3 4 = 7 rflAll goals completed! 🐙
example : doIt3Times plus3 0 = 9 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times plus3 0 = 9 rflAll goals completed! 🐙
example : doIt3Times (Nat.add 3) 0 = 9 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (Nat.add 3) 0 = 9 rflAll goals completed! 🐙

plus3 : Nat → Nat

Similarly, we can write:

def fold_plus : List Nat → Nat → Nat :=
  fold (· + ·)

fold_plus : List Nat → Nat → Nat#check fold_plus

fold_plus : List Nat → Nat → Nat

6.3. Additional Exercises🔗

6.3.1. Church Numerals (Advanced)🔗

Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC