The goal of this lecture note is to describe how polymorphism is rendered and used in Gallina.
“morph” means “shape” and “poly” means “several” in Greek. So literally, something is polymorphic if it has several shapes. And likewise, something is monomorphic if it has one shape.
Gallina is a polymorphically typed programming language in that the type of an expression can contain type variables that are explicitly declared with a “forall” quantifier:
t ::= nat | bool | ... | t * t | t * ... * t | t -> t | ... | x | Type | forall x : Type, t | ...
So the type of the pairing function reads:
forall A : Type, forall B : Type, A -> B -> A * B
In practice, this type is syntactically sugared as:
forall (A : Type) (B : Type), A -> B -> A * B
So in Gallina, polymorphic types are parameterized types: the type variables are declared.
Here are several implementations of the pairing function, using an increasing amount of syntactic sugar:
Definition make_pair_v0 : forall (A : Type) (B : Type), A -> B -> A * B :=
fun (A : Type) (B : Type) (a : A) (b : B) => (a, b).
Definition make_pair_v1 (A : Type) : forall B : Type, A -> B -> A * B :=
fun (B : Type) (a : A) (b : B) => (a, b).
Definition make_pair_v2 (A : Type) (B : Type) : A -> B -> A * B :=
fun (a : A) (b : B) => (a, b).
Definition make_pair_v3 (A : Type) (B : Type) (a : A) : B -> A * B :=
fun (b : B) => (a, b).
Definition make_pair_v4 (A : Type) (B : Type) (a : A) (b : B) : A * B :=
(a, b).
So in Gallina, polymorphic functions are parameterized with a type.
Instantiating a type variable is achieved by applying a polymorphic function to that type. So for example tCPA processes Compute (make_pair_v4 nat bool 1 true). by emitting = (1, true) : nat * bool in the *response* window. Likewise for a function that duplicates its argument into a pair:
Definition duplicate (V : Type) (v : V) : V * V :=
make_pair_v4 V V v v.
Gallina also features polymorphic data types in that we can parameterize data-type declarations with type variables. For example, a polymorphic binary trees with payloads in the leaves is declared as follows:
Inductive polymorphic_binary_tree (V : Type) : Type :=
PLeaf : V -> polymorphic_binary_tree V
| PNode : polymorphic_binary_tree V -> polymorphic_binary_tree V -> polymorphic_binary_tree V.
Each constructor now is parameterized with a type.
This parameterization makes it possible – unlike in OCaml – to define polymorphic unit-test functions:
Definition test_number_of_leaves (candidate : forall V : Type, polymorphic_binary_tree V -> nat) :=
true
&&
(candidate bool (PLeaf bool true) =? 1)
&&
(candidate nat (PNode nat (PLeaf nat 0) (PLeaf nat 1)) =? 2).
A function that processes a polymorphic binary tree is itself polymorphic. The match-expression that is used to dispatch on PLeaf and PNode requires us to put a placeholder for the type parameter. Otherwise, it is business as usual, a structurally recursive function:
Fixpoint number_of_leaves (V : Type) (t : polymorphic_binary_tree V) : nat :=
match t with
PLeaf _ v =>
1
| PNode _ t1 t2 =>
number_of_leaves V t1 + number_of_leaves V t2
end.
To compare polymorphic binary trees, we parameterize the comparison function with a comparison function for its payloads:
Fixpoint eqb_polymorphic_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
match t1 with
PLeaf _ v1 =>
match t2 with
PLeaf _ v2 =>
eqb_V v1 v2
| PNode _ t11 t12 =>
false
end
| PNode _ t11 t12 =>
match t2 with
PLeaf _ v2 =>
false
| PNode _ t21 t22 =>
eqb_polymorphic_binary_tree V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree V eqb_V t12 t22
end
end.
This comparison function is defined recursively on its first argument and by cases on its second argument.
Pablito: Structural equality?
Dana: “Structural” means “that follows the structure”.
Bong-sun: So eqb_polymorphic_binary_tree recursively tests whether the two given trees have the same structure...
Dana: ...and if they do, whether the payloads in the leaves are equal...
Pablito: ...using eqb_V, the given equality predicate at type V, I can see that, thanks.
Halcyon: Er... Shouldn’t we implement a unit-test function first?
Alfrothul: Indeed we should, Halcyon. Indeed we should. Do you want to implement one?
Halcyon (honestly): I am not completely sure how to do that.
Pablito: May I?
Halcyon: Please.
Pablito: First, we need to name it meaningfully. Here, meaningful means that its name is test_ followed by the name of the function we want to test:
Definition test_eqb_polymorphic_binary_tree ...
Halcyon: OK.
Pablito: Then, we parameterize it with the candidate function we want to test:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
true
&&
...
Halcyon: And the result of the unit-test function is a boolean, OK.
Pablito: Right. Then, the body of the function is a conjunction of tests. For example, we can test whether applying the candidate function to two leaves with the same payload yields true:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
true
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
...
Halcyon: OK.
Pablito: We can also test whether applying the candidate function to two nodes that contain the same leaves also yields true:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
true
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0))
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0)))
true).
Pablito: It’s not a very good unit-test function, but you see its structure?
Halcyon: I see its structure, but why is it not a very good unit-test function?
Pablito: Because we can easily defeat it with a fake candidate function. For example, the constant candidate function that always returns true passes the tests, look:
Compute (test_eqb_polymorphic_binary_tree
(fun (V : Type)
(eqb_V : V -> V -> bool)
(t1 t2 : polymorphic_binary_tree V) =>
true)).
Halcyon: Right – the *response* window reads:
= true
: bool
Pablito: So we need to also have negative tests in the conjunction.
Halcyon: Negative tests?
Pablito: Tests that not only check that the candidate function returns true when it should – these are positive tests, but also tests that check that the candidate function returns false when it should – these are negative tests. Let me add a negative test with two leaves that do not have the same payload:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
true
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 1))
false)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0))
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0)))
true).
Halcyon: Ah, OK.
Pablito: But we are not done yet.
Halcyon: We are not done?
Pablito: We are not.
Halcyon: Why are we not done?
Pablito: Because our unit tests must provide code coverage.
Halcyon: Code what?
Pablito: Coverage. Code coverage. All the conditional branches of the program should be evaluated when the unit-test function is applied.
Halcyon: And the unit-test function you just implement doesn’t provide code coverage?
Pablito: It doesn’t. For example, look at the clause in the base case:
match t2 with
PLeaf _ v2 =>
eqb_V v1 v2
| PNode _ t11 t12 =>
false
end
Pablito (continuing): The conditional branch false is not evaluated during the tests because the candidate function is not applied to a leaf and a node.
Bong-sun: May I be pedantic for a second?
Pablito: Sure.
Bong-sun: Suppose that the conditional branch eqb_V v1 v2 is written as a conditional expression:
match t2 with
PLeaf _ v2 =>
if eqb_V v1 v2
then true
else false
| PNode _ t11 t12 =>
false
end
Pablito: OK, that’s pedantic.
Bong-sun: It is, but it also makes it explicit that there are two conditional branches when both the given trees are leaves.
Pablito: True, that.
Bong-sun: And it also makes it clear that your unit tests provide code coverage there, since they both test the case where the two given trees are the same leaves and the case where the two given trees are not the same leaves.
Loki: So there is something to be said for being pedantic.
Mimer: Sometimes, yes.
Pablito: Anyway, we should also test the case where the candidate function is applied to a leaf and a node:
...
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PNode
nat
(PLeaf nat 1)
(PLeaf nat 2)))
false)
&&
...
Halcyon: I am guessing that we should also test the case where the candidate function is applied to a node and a leaf:
...
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 1)
(PLeaf nat 2))
(PLeaf nat 0))
false)
&&
...
Pablito: Indeed we should, thanks.
Bong-sun: And then regarding the boolean conjunction in the induction step, there are four possibilities, so there should be four tests.
Pablito: Huh, can I be pedantic for a second?
Bong-sun: By all means. What do you have in mind?
Pablito: Well, a boolean conjunction e1 && e2 is syntactic sugar for if e1 then e2 else false, so we can make it clear that the last match clause contains four conditional branches.
Bong-sun: Can you tell me more?
Pablito: Yes of course. Look at the last match clause:
eqb_polymorphic_binary_tree V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree V eqb_V t12 t22
Bong-sun: OK.
Pablito: Here it is again, desugared:
if eqb_polymorphic_binary_tree V eqb_V t11 t21
then eqb_polymorphic_binary_tree V eqb_V t12 t22
else false
Bong-sun: Yes?
Pablito: And now all we need to do is to write each call to the predicate as a conditional expression:
if if eqb_polymorphic_binary_tree V eqb_V t11 t21
then true
else false
then if eqb_polymorphic_binary_tree V eqb_V t12 t22
then true
else false
else false
Pablito: Hum, wait, now there are five booleans.
Bong-sun: Yes.
Pablito: Let me be a bit less pedantic and only write the second call to the predicate as a conditional expression, since the first one already occurs as a test in a conditional expression:
if eqb_polymorphic_binary_tree V eqb_V t11 t21
then if eqb_polymorphic_binary_tree V eqb_V t12 t22
then true
else false
else false
Pablito: Hum. Three booleans. But I was expecting four?
Bong-sun: That is because false is absorbing for boolean conjunction, and that is captured in the syntactic sugar for &&. In e1 && e2, e2 is only evaluated when e1 evaluates to true. Computationally, this property is known as short-circuit evaluation. It’s a thing.
Pablito: So?
Bong-sun: So OK, there are only three possibilities. It was good of you to be pedantic. Thanks, Pablito.
Pablito (blushing): Er... Thank you.
Halcyon: And then that’s it?
Pablito: Yes, that’s it: all the possibilities are covered in the unit-test function.
Mimer: Which is why “code coverage” is also referred to as “test coverage”.
In the resource file, complete test_eqb_polymorphic_binary_tree so that it provides code coverage for eqb_polymorphic_binary_tree, and recapitulate why it does.
Anton: Question.
Mimer: Yes, Anton?
Anton: My implementation of eqb_polymorphic_binary_tree is a lot simpler, look:
Fixpoint eqb_polymorphic_binary_tree' (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
match (t1, t2) with
(PLeaf _ v1, PLeaf _ v2) =>
eqb_V v1 v2
| (PNode _ t11 t12, PNode _ t21 t22) =>
eqb_polymorphic_binary_tree' V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree' V eqb_V t12 t22
| _ =>
false
end.
Mimer: Indeed it it a lot shorter.
Anton: Simpler too, no?
Mimer: Well, prima facie it is less efficient.
Anton: Less efficient?
Mimer: Well, yes – at each call, an intermediate pair is constructed and then immediately deconstructed.
Anton: Well, I am trusting the compiler to optimize that away.
Mimer: But then what you see is not what you get, and the point here is to acquire a sense of reasoning about what we write.
Anton: Harrumph.
Mimer: And then there is the point of understanding what we program. In the declaration above, it is clear that the predicate is defined recursively over its first argument and by cases on its second argument. But here, it looks like the predicate is defined recursively over both its arguments, which is a lot more complicated if that were to be the case.
Anton: On the other hand, my definition makes it simpler to enumerate all the possible cases to have code coverage in the unit-test function.
Mimer (diplomatic): That it might.
Anton: But I see your point.
Mimer: And you will see it even more in Week 03, when we start to reason about recursive functions over binary trees.
Anton: Looking forward to it.
For example, a function testing the structural equality of binary trees of natural numbers is obtained by instantiating eqb_polymorphic_binary_tree with the type of natural numbers and the equality predicate for natural numbers:
Definition eqb_nat := Nat.eqb.
Definition eqb_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree nat) : bool :=
eqb_polymorphic_binary_tree nat eqb_nat t1 t2.
And a function testing the structural equality of binary trees of booleans is obtained by instantiating eqb_polymorphic_binary_tree with the type of booleans and the equality predicate for booleans:
Definition eqb_bool := Bool.eqb.
Definition eqb_binary_tree_of_bools (t1 t2 : polymorphic_binary_tree bools) : bool :=
eqb_polymorphic_binary_tree bool eqb_bool t1 t2.
Anton: This exercise is a straight followup of Exercise 04, isn’t it?Alfrothul: Looks like, Anton. Looks like.Pablito: So we need to implement several recursive functions?Alfrothul: Doesn’t look like, Pablito. Doesn’t look like.Pablito: How so?Anton: Well, look at the definitions of eqb_binary_tree_of_nats and of eqb_binary_tree_of_bools.
As in OCaml, the option type and its constructors Some and None exists in Gallina. So for example, Some 2 has type option nat, which we can verify with the Check command:
Check (Some 2).
The *response* window now contains:
Some 2
: option nat
As in the section about a practical use of the Check command in Week 01, we can use the Check command when we need to exhibit an expression that has a given type.
Here are some examples of this use:
Say we are asked to exhibit an expression that has type option (nat * bool). We know that an optional value is constructed with the Some constructor, so all we need is an expression of type nat * bool. But we know since Week 01 (in the section about a practical use of the Check command to be precise) how to construct such an expression, e.g., (1, false). So our putative expression is Some (1, false), which we can verify using the Check command:
Check (Some (1, false)).
The *response* window now contains:
Some (1, false)
: option (nat * bool)
This content manifests that Some (1, false) has type option (nat * bool), and so this expression can be one that we can exhibit.
Say we are asked to exhibit an expression that has type option (option bool). We know that optional values are constructed using the Some constructor – i.e., as something like Some ..., so all that we need is to exhibit an expression that has type option bool. Again, we know that optional values are constructed using the Some constructor – i.e., as something like Some ..., so all that we need is to exhibit an expression that has type bool, e.g., false.
All in all, we posit that Some (Some false) has type option (option bool), and we verify this claim using the Check command:
Check (Some (Some false)).
The *response* window now contains:
Some (Some false)
: option (option bool)
This content manifests that our putative expression has the required type, and so this expression can be one that we can exhibit.
Say we are asked to exhibit an expression that has type option nat -> bool.
We know that functions are constructed using the fun keyword and that the domain of option nat -> bool is option nat. So the type of the formal parameter has to be option nat, and our putative expression can start with fun (on : option nat) => ....
Now instead of ..., we need to exhibit an expression of type bool. We could just write true or false, but let us playfully implement a function that uses its argument. For example, let us make it map Some n to true and None to false. To this end, we need to distinguish how the argument of the function was constructed. So instead of ..., we write a match expression:
match on with
Some n =>
...
| None =>
...
end
And then in the Some clause we return true and in the None clause we return false:
match on with
Some n =>
true
| None =>
false
end
All in all, we posit that fun (on : option nat) => match on with Some n => true | None => false end has type option nat -> bool, and we verify this claim using the Check command:
Check (fun (on : option nat) => match on with Some n => true | None => false end).
The *response* window now contains:
fun on : option nat => match on with
| Some _ => true
| None => false
end
: option nat -> bool
This content manifests that our putative expression has the required type, and so this expression can be one that we can exhibit.
In the line of Section Structural equality of polymorphic binary trees,
implement a comparison function for optional values:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
...
implement a function testing the structural equality of optional binary trees of natural numbers:
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
...
implement a function testing the structural equality of optional binary trees of optional natural numbers:
Definition eqb_optional_binary_tree_of_optional_nats (t1 t2 : option (polymorphic_binary_tree (option nat))) : bool :=
...
implement a function testing the structural equality of binary trees of optional binary trees of natural numbers:
Definition eqb_binary_tree_of_optional_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree nat))) : bool :=
...
implement a function testing the structural equality of binary trees of optional binary trees of optional natural numbers:
Definition eqb_binary_tree_of_optional_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree (option nat)))) : bool :=
...
Bong-sun: Let’s see. The option type is a sum...
Dana: ...so the comparison function is defined by cases:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
...
end
| None =>
match ov2 with
Some v =>
...
| None =>
...
end
end.
Pablito: When the two given arguments are not constructed with the same constructor, they are not equal:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
false (* <--- *)
end
| None =>
match ov2 with
Some v =>
false
| None =>
...
end
end.
Anton: And when they both are None, they are equal:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
false
end
| None =>
match ov2 with
Some v =>
false
| None =>
true (* <--- *)
end
end.
Halcyon: Which leaves us with the case where they are both constructed with Some.
Alfrothul: So if the first argument is Some v1 and if the second argument is Some v2, they are equal whenever v1 and v2 are equal. Luckily eqb_option is parameterized with the equality predicate eqb_V, so let’s use it:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
eqb_V v1 v2 (* <--- *)
| None =>
false
end
| None =>
match ov2 with
Some v =>
false
| None =>
true
end
end.
Mimer: Tadaa!
Dana: Now for implementing an equality predicate for optional binary trees of natural numbers... We are going to use eqb_option at type polymorphic_binary_tree nat.
Bong-sun (practical): Let’s see:
Check (eqb_option (polymorphic_binary_tree nat)).
Pablito (diligent): The *response* window reads:
eqb_option (polymorphic_binary_tree nat)
: (polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool) ->
option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool
Anton: Aha. So all we need is something of type polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool.
Alfrothul: Presto:
Check (eqb_polymorphic_binary_tree nat eqb_nat).
Pablito (dutiful): The *response* window reads:
eqb_polymorphic_binary_tree nat eqb_nat
: polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool
Bong-sun: So here we go:
Check (eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat)).
Pablito (happily): The *response* window reads:
eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat)
: option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool
Dana: So we are done here:
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat) t1 t2.
Halcyon: But we have defined eqb_binary_tree_of_nats already, haven’t we?
Dana: Well spotted, Halcyon:
Definition eqb_optional_binary_tree_of_nats' (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1 t2.
Bong-sun: Actually, we don’t need to declare t1 and t2, look:
Definition eqb_optional_binary_tree_of_nats'' : option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats.
Dana: Or we could just declare t1, look:
Definition eqb_optional_binary_tree_of_nats''' (t1 : option (polymorphic_binary_tree nat)) : option (polymorphic_binary_tree nat) -> bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1.
Alfrothul: The marvels of syntactic sugar:
Definition eqb_optional_binary_tree_of_nats'''' (t1 : option (polymorphic_binary_tree nat)) (t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1 t2.
Pablito: This is fun.
Halcyon: Yup.
Declare a polymorphic data type of binary trees with payloads in the nodes, implement a function that counts the nodes in a given tree, and test it using a unit-test function that features trees of different types. Implement also a polymorphic predicate that tests the structural equality of two binary trees with payloads in the nodes, along with unit tests that provide code coverage.
Declare a polymorphic data type of binary trees with payloads both in the leaves and in the nodes, implement a function that computes the height of a given tree, and test it using a unit-test function that features trees of different types. Implement also a polymorphic predicate that tests the structural equality of two binary trees with payloads both in the leaves and in the nodes.
Having to pass a type parameter to every polymorphic constructor and function tends to become tiresome after a while, and so tCPA features some magic to declare implicit parameters.
For example, the option type and its constructors Some and None pre-exist, and it is a polymorphic data type, in that, e.g., (Some 10, Some true) has type option nat * option bool.
On the other hand, if we were to declare our own option type, we would need to pass a type parameter to the constructors:
Inductive option' (V : Type) : Type :=
Some' : V -> option' V
| None' : option' V.
Namely, we would need to write, e.g., (Some' nat 10, Some' bool true), which has type option' nat * option' bool.
The reason for Some needing no type parameter is that the declaration of the option type, in the initial library, was preceded by:
Set Implicit Arguments.
For example, let us now declare:
Inductive option'' (V : Type) : Type :=
Some'' : V -> option'' V
| None'' : option'' V.
Since this declaration was preceded by Set Implicit Arguments., the type parameter is now implicit, and (Some'' 10, Some'' true) has type option nat * option bool: the type argument has been inferred from the context.
What about None, None', and None'' then? Here is what the Check command says:
(Incidentally, to specify that we are wish for an instance of None at a particular type, say, nat, we write (@None nat)).
Warning
Reformatted the unit-test functions uniformly [16 Feb 2025]
Added a section about the polymorphic option type, belatedly [02 Feb 2025]
Expanded the exchange about the induction step in the interlude about the equality predicate for polymorphic binary trees [25 Jan 2025]
Created [24 Jan 2025]