Mercurial > hg > Gears > GearsAgda

diff stack.agda @ 554:988c12d7f887

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use another nat comparator
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Mar 2018 23:22:07 +0900
parents 4f692df9b3db
children 70b09cbefd45
line wrap: on
line diff
--- a/stack.agda	Mon Mar 26 17:50:04 2018 +0900
+++ b/stack.agda	Mon Mar 26 23:22:07 2018 +0900
@@ -17,6 +17,10 @@
     pi1 : a
     pi2 : b
 
+data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where
+   pi1  : a -> a ∨ b
+   pi2  : b -> a ∨ b
+
 data Maybe {n : Level } (a : Set n) : Set n where
   Nothing : Maybe a
   Just    : a -> Maybe a