git.iko.soy/Idris-dev
on master help sign in
Add syntax for Agda-style reasoning over preorders
93f03deDavid Christiansen
libs/base/Syntax/PreorderReasoning.idrnew file+15
compare with master
unifiedsplit
@@ -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,
16
16
17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
18
18
19− Data.Morphisms,
19+ Data.Morphisms,
20− Data.Bits, Data.Mod2,
20+ Data.Bits, Data.Mod2,
21 Data.ZZ, Data.Sign,
21 Data.ZZ, Data.Sign,
22 Data.SortedMap, Data.SortedSet, Data.BoundedList,
22 Data.SortedMap, Data.SortedSet, Data.BoundedList,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
@@ -27,4 +27,6 @@ modules = System,
27 Control.Monad.RWS,
27 Control.Monad.RWS,
28 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
28 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
29 Control.Category, Control.Arrow,
29 Control.Category, Control.Arrow,
30− Control.Catchable, Control.IOExcept
30+ Control.Catchable, Control.IOExcept,
31+
32+ Syntax.PreorderReasoning