summaryrefslogtreecommitdiffstats log msg author committer range
diff options
 context: 12345678910152025303540 space: includeignore mode: unifiedssdiffstat only
author committer Thomas Letan 2020-07-12 11:23:03 +0200 Thomas Letan 2020-07-12 12:24:49 +0200 cec5638c1a23303723464bf5f73cea475fb4d94c (patch) f824ae765a9d3c4b68e7d9f168b9929f198f5f29 /site/posts/AlgebraicDatatypes.v 41007fce2a333ba78be703c35f4afccade3369e5 (diff)
Spellchecking
Diffstat (limited to 'site/posts/AlgebraicDatatypes.v')
-rw-r--r--site/posts/AlgebraicDatatypes.v22
1 files changed, 10 insertions, 12 deletions
 diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.vindex b5a786f..74bdf04 100644--- a/site/posts/AlgebraicDatatypes.v+++ b/site/posts/AlgebraicDatatypes.v@@ -22,7 +22,7 @@ data List a = << enum List {- Cons(A, Box),+ Cons(A, Box< List >), Nil, } >>@@ -57,7 +57,7 @@ Inductive list a := Therefore, a datatype with several constructors is reminescent of a disjoint union. Coming back to the [list] type, under the syntactic sugar of algebraic datatypes, the [list α] type is equivalent to [unit + α * list α],- where [unit] models the [nil] case, and [α + list α] models the [cons] case.+ where [unit] models the [nil] case, and [α * list α] models the [cons] case. The set of types which can be defined in a language together with [+] and [*] form an “algebraic structure” in the mathematical sense, hence the@@ -118,13 +118,11 @@ Set Implicit Arguments. (** *** Introducing [type_equiv] *) (** Since [=] for [Type] is not suitable for reasoning about algebraic- datatypes. As a consequence, we first introduce our own equivalence- relation, denoted [==].-- We say two types [α] and [β] are equivalent up to an isomorphism (denoted by- [α == β]) when for any term of type [α], there exists a counter-part term of- type [β] and vice versa. In other words, [α] and [β] are equivalent if we- can exhibit two functions [f] and [g] such that:+ datatypes, we introduce our own equivalence relation, denoted [==]. We say+ two types [α] and [β] are equivalent up to an isomorphism (denoted by [α ==+ β]) when for any term of type [α], there exists a counter-part term of type+ [β] and vice versa. In other words, [α] and [β] are equivalent if we can+ exhibit two functions [f] and [g] such that: ##\forall (x : α),\ x = g(f(x))## @@ -136,8 +134,8 @@ Reserved Notation "x == y" (at level 72). Inductive type_equiv (α β : Type) : Prop := | mk_type_equiv (f : α -> β) (g : β -> α)- (equ1 : forall (x : α), x = g (f x))- (equ2 : forall (y : β), y = f (g y))+ (equ1 : forall (x : α), x = g (f x))+ (equ2 : forall (y : β), y = f (g y)) : α == β where "x == y" := (type_equiv x y). @@ -306,7 +304,7 @@ Qed. (** **** Non-empty Lists *) -(** We can introduce a variant of [list] which contains at least one element, by+(** We can introduce a variant of [list] which contains at least one element by modifying the [nil] constructor so that it takes one argument instead of none. *)