From 4032974f05f80cbab61a26f4b30ce57ec2e43b3b Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 8 Aug 2022 09:48:04 +0100 Subject: Snapshot --- doc/sources/Tutorial.md | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'doc/sources/Tutorial.md') 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 -- cgit v1.2.3