git.iko.soy/Idris-dev
on master help sign in
Add syntax for Agda-style reasoning over preorders
commit93f03ded7ff818829b0cae03600880c15026267b authorDavid Christiansen <david@davidchristiansen.dk> dateSun 15 Dec 2013, 11:37 (13 years ago) parent8695646
2 files changed+20−3
compare with master
unifiedsplit
libs/base/Syntax/PreorderReasoning.idr+15 libs/base/base.ipkg+5−3
libs/base/Syntax/PreorderReasoning.idrnew file+15
@@ -0,0 +1,15 @@
1+module Syntax.PreorderReasoning
2+
3+-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
4+syntax [expr] "QED" = qed expr
5+-- foo ={ prf }= bar ={ prf' }= fnord QED
6+-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
7+syntax [from] "={" [prf] "}=" [to] = step from prf to
8+
9+namespace Equal
10+ using (a : Type, x : a, y : a, z : a)
11+ qed : (x : a) -> x = x
12+ qed x = the (x = x) refl
13+ step : (x : a) -> x = y -> (y = z) -> x = z
14+ step x refl refl = refl
15+
libs/base/base.ipkg+5−3
@@ -16,8 +16,8 @@ modules = System,
1616
1717 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
1818
19− Data.Morphisms,
20− Data.Bits, Data.Mod2,
19+ Data.Morphisms,
20+ Data.Bits, Data.Mod2,
2121 Data.ZZ, Data.Sign,
2222 Data.SortedMap, Data.SortedSet, Data.BoundedList,
2323 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
@@ -27,4 +27,6 @@ modules = System,
2727 Control.Monad.RWS,
2828 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
2929 Control.Category, Control.Arrow,
30− Control.Catchable, Control.IOExcept
30+ Control.Catchable, Control.IOExcept,
31+
32+ Syntax.PreorderReasoning