diff options
| author | Iain Lane <laney@debian.org> | 2011-11-29 16:51:32 +0000 |
|---|---|---|
| committer | Iain Lane <laney@debian.org> | 2011-11-29 16:51:32 +0000 |
| commit | becce68e992af760dbdc6f17e77bc4dfeecccef7 (patch) | |
| tree | fe929e2d8863fe17c1c2909283e1442b6f4a3286 /src/Relation/Binary/EqReasoning.agda | |
| parent | 9251e0b00e309e805a4576ae558b3d1e321d8f2c (diff) | |
Imported Upstream version 0.6~darcs20111129t1640
Diffstat (limited to 'src/Relation/Binary/EqReasoning.agda')
| -rw-r--r-- | src/Relation/Binary/EqReasoning.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Relation/Binary/EqReasoning.agda b/src/Relation/Binary/EqReasoning.agda index 44321d1..d56716d 100644 --- a/src/Relation/Binary/EqReasoning.agda +++ b/src/Relation/Binary/EqReasoning.agda @@ -1,9 +1,9 @@ ------------------------------------------------------------------------ +-- The Agda standard library +-- -- Convenient syntax for equational reasoning ------------------------------------------------------------------------ -{-# OPTIONS --universe-polymorphism #-} - -- Example use: -- n*0≡0 : ∀ n → n * 0 ≡ 0 |