diff options
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 |