From e84fe1bb1f4fe7f8989b18b2fba7cee7149c39a2 Mon Sep 17 00:00:00 2001
From: mangoiv <contact@mangoiv.com>
Date: Sat, 30 Nov 2024 14:49:06 +0100
Subject: [PATCH] [chore] some spelling corrections

---
 examples/tutorial.pol | 42 ++++++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 20 deletions(-)

diff --git a/examples/tutorial.pol b/examples/tutorial.pol
index a56ca847c..8a5b8b6f7 100644
--- a/examples/tutorial.pol
+++ b/examples/tutorial.pol
@@ -1,25 +1,26 @@
--- We can define the data type Bool with constructors T and F
+-- We can define the data type Bool with constructors T and F.
 data Bool { T, F }
 
--- We can define the not operator by case distinction
+-- We can define the not operator by case distinction.
 def Bool.not: Bool {
     T => F,
     F => T
 }
 
--- We can define the if_then_else operation
+-- We can define the if_then_else operation.
 def Bool.if_then_else(a: Type, then else: a): a {
     T => then,
     F => else
 }
 
 -- Since polarity is dependently typed, we can return different types,
+-- depending on the value of the Bool that is scrutinized.
 def (b : Bool).dep_if_then_else(t1 t2: Type, then: t1, else: t2): b.if_then_else(Type, t1, t2){
   T => then,
   F => else
 }
 
--- We can simple define recursive datatypes
+-- We can define simple recursive data types.
 data Nat { Z, S(n: Nat) }
 
 def Nat.add(y: Nat): Nat {
@@ -27,7 +28,7 @@ def Nat.add(y: Nat): Nat {
     S(x') => S(x'.add(y))
 }
 
--- And more complex, parametrised ones, like this classic
+-- And more complex, parametrised ones, like this classic.
 data Vec(n: Nat) {
     VNil: Vec(Z),
     VCons(n x: Nat, xs: Vec(n)): Vec(S(n))
@@ -36,19 +37,19 @@ data Vec(n: Nat) {
 -- So far so good. We have covered a bunch of examples in a simple, dependently typed
 -- language. But what makes polarity special?
 
--- Polarity allows to define codata types
--- They do not tell you what they are made of, but how you observe them
+-- Polarity allows to define codata types.
+-- They do not tell you what they are made of, but how you observe them.
 -- If you look at a stream, for example, you can either observe its head,
 -- which in this case is just a natural number, or its tail, which is,
--- once again, a Stream
+-- once again, a Stream.
 codata Stream { .head: Nat, .tail: Stream }
 
--- Since polarity does not have a function type, we have to use codata types to build it
--- ourselves. This specific one is specialised to Nats.
+-- Since polarity does not have a function type. Instead, we have to use codata
+-- types to build it ourselves. This specific one is specialised to Nats.
 codata NatToNat { .ap(x: Nat): Nat }
 
 -- A simple value of this type would be the function that returns the predecessor of a
--- Nat, or Zero if the Nat is already Zero. To build values of codata types, we use codef
+-- Nat, or Zero if the Nat is already Zero. To build values of codata types, we use codef:
 codef Pred: NatToNat {
   -- if we observe the application of a function of Nat to Nat
   .ap(n) => n.match { -- we case split on the Nat
@@ -57,45 +58,46 @@ codef Pred: NatToNat {
   }
 }
 
--- This is the main entry point for running programs in polarity
--- When invoking pol run tutorial.pol, this will print S(S(S(S(Z)))) 
+-- This definition (main) is the main entry point for running programs 
+-- in polarity. When invoking pol run tutorial.pol, this will print S(S(S(S(Z)))) 
 -- (also known as 4) as expected
 let main: Nat { Pred.ap(2.add(3)) }
 
 -- Now that we covered all the basics, lets look at some more examples:
 
--- We can build an option type that may (Some) or may not (None) contain a value
+-- We can build an option type that may (Some) or may not (None) contain a value.
 data Option(a: Type) {
     None(a: Type): Option(a),
     Some(a: Type, x: a): Option(a)
 }
 
--- We can also build simple, non-dependent Lists, as a datatype
+-- We can also build simple, non-dependent Lists, as a data type.
 data List(a: Type) {
     Nil(a: Type): List(a),
     Cons(a: Type, x: a, xs: List(a)): List(a)
 }
 
--- And of course write a (safe) head implementation for it
+-- And of course write a (safe) head implementation for it.
 def List(a).hd(a: Type): Option(a) {
     Nil(a) => None(a),
     Cons(a, x, xs) => Some(a, x)
 }
 
--- We can build different kinds of (infinite) streams
--- One that contains only Zeroes
+-- We can build different kinds of (infinite) streams.
+
+-- One that contains only Zeroes:
 codef Zeroes: Stream {
     .head => Z,
     .tail => Zeroes
 }
 
--- One that contains only Ones
+-- One that contains only Ones:
 codef Ones: Stream {
     .head => S(Z),
     .tail => Ones
 }
 
--- And one that alternates between Ones and Zeroes
+-- And one that alternates between Ones and Zeroes:
 codef Alternate(choose: Bool): Stream {
     .head => choose.if_then_else(Nat, S(Z), Z),
     .tail => Alternate(choose.not)