diff options
Diffstat (limited to 'doc/sources/Tutorial.md')
| -rw-r--r-- | doc/sources/Tutorial.md | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md index 85b09c8..a33652f 100644 --- a/doc/sources/Tutorial.md +++ b/doc/sources/Tutorial.md @@ -200,15 +200,19 @@ This proof is a lot more involved: 1. We appeal to the cancellation property of addition: $a + c = b + c \Rightarrow a = b$ + + This construction relies crucially on the cancellation property. Later, we + will learn about its general form, called the INT-construction. + 2. We rearrange the term, bringing the appropriate part of `y` into contact with the appropriate part of `z` and `x` to transform the term. -Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex) -that can perform such routine -rearrangements for common algebraic structures. In this case, we use the -commutative monoid simplifier from `Frex`. -If you want to read more about `Frex`, check the -[paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out. + Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex) + that can perform such routine + rearrangements for common algebraic structures. In this case, we use the + commutative monoid simplifier from `Frex`. + If you want to read more about `Frex`, check the + [paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out. Idris's `Control.Relation` defines interfaces for properties like reflexivity |