diff options
| author | Gabor Pali <pgj@FreeBSD.org> | 2015-08-20 23:02:14 +0000 |
|---|---|---|
| committer | Gabor Pali <pgj@FreeBSD.org> | 2015-08-20 23:02:14 +0000 |
| commit | 39b8e49140afdb1d1d001c477befb4b05efa7fc3 (patch) | |
| tree | 607a5ca77efd301a2b4dc49b05d108829fcffa77 /math/hs-Agda-stdlib/files/patch-src_Size.agda | |
| parent | 75b64b1cb42c127b71646f039269eb7bd560d8ef (diff) | |
| download | ports-39b8e49140afdb1d1d001c477befb4b05efa7fc3.tar.gz ports-39b8e49140afdb1d1d001c477befb4b05efa7fc3.zip | |
Notes
Diffstat (limited to 'math/hs-Agda-stdlib/files/patch-src_Size.agda')
| -rw-r--r-- | math/hs-Agda-stdlib/files/patch-src_Size.agda | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/math/hs-Agda-stdlib/files/patch-src_Size.agda b/math/hs-Agda-stdlib/files/patch-src_Size.agda new file mode 100644 index 000000000000..7b141b5a8577 --- /dev/null +++ b/math/hs-Agda-stdlib/files/patch-src_Size.agda @@ -0,0 +1,21 @@ +--- src/Size.agda.orig 2014-11-14 23:18:11 UTC ++++ src/Size.agda +@@ -6,13 +6,8 @@ + + module Size where + +-postulate +- Size : Set +- Size<_ : Size → Set +- ↑_ : Size → Size +- ∞ : Size +- +-{-# BUILTIN SIZE Size #-} +-{-# BUILTIN SIZELT Size<_ #-} +-{-# BUILTIN SIZESUC ↑_ #-} +-{-# BUILTIN SIZEINF ∞ #-} ++{-# BUILTIN SIZEUNIV SizeUniv #-} -- sort SizeUniv ++{-# BUILTIN SIZE Size #-} -- Size : SizeUniv ++{-# BUILTIN SIZELT Size<_ #-} -- Size<_ : Size → SizeUniv ++{-# BUILTIN SIZESUC ↑_ #-} -- ↑_ : Size → Size ++{-# BUILTIN SIZEINF ∞ #-} -- ∞ : Size |