Permalink
Browse files

Agda standard library 0.2

  • Loading branch information...
1 parent e05491a commit b72c796b441e6d30ca96697d0c3d34a91408302a Larry Diehl committed Apr 27, 2010
Showing with 18,107 additions and 0 deletions.
  1. +5 −0 vendor/stdlib/.boring
  2. +27 −0 vendor/stdlib/AllNonAsciiChars.hs
  3. +480 −0 vendor/stdlib/Everything.agda
  4. +8 −0 vendor/stdlib/GNUmakefile
  5. +87 −0 vendor/stdlib/GenerateEverything.hs
  6. +7 −0 vendor/stdlib/Header
  7. +22 −0 vendor/stdlib/LICENCE
  8. +257 −0 vendor/stdlib/README.agda
  9. +16 −0 vendor/stdlib/README.txt
  10. +54 −0 vendor/stdlib/README/Nat.agda
  11. +26 −0 vendor/stdlib/release-notes
  12. +470 −0 vendor/stdlib/src/Algebra.agda
  13. +85 −0 vendor/stdlib/src/Algebra/FunctionProperties.agda
  14. +19 −0 vendor/stdlib/src/Algebra/FunctionProperties/Core.agda
  15. +47 −0 vendor/stdlib/src/Algebra/Morphism.agda
  16. +58 −0 vendor/stdlib/src/Algebra/Operations.agda
  17. +36 −0 vendor/stdlib/src/Algebra/Props/AbelianGroup.agda
  18. +552 −0 vendor/stdlib/src/Algebra/Props/BooleanAlgebra.agda
  19. +62 −0 vendor/stdlib/src/Algebra/Props/DistributiveLattice.agda
  20. +43 −0 vendor/stdlib/src/Algebra/Props/Group.agda
  21. +47 −0 vendor/stdlib/src/Algebra/Props/Lattice.agda
  22. +36 −0 vendor/stdlib/src/Algebra/Props/Ring.agda
  23. +237 −0 vendor/stdlib/src/Algebra/RingSolver.agda
  24. +119 −0 vendor/stdlib/src/Algebra/RingSolver/AlmostCommutativeRing.agda
  25. +116 −0 vendor/stdlib/src/Algebra/RingSolver/Lemmas.agda
  26. +11 −0 vendor/stdlib/src/Algebra/RingSolver/Simple.agda
  27. +334 −0 vendor/stdlib/src/Algebra/Structures.agda
  28. +17 −0 vendor/stdlib/src/Category/Applicative.agda
  29. +42 −0 vendor/stdlib/src/Category/Applicative/Indexed.agda
  30. +18 −0 vendor/stdlib/src/Category/Functor.agda
  31. +29 −0 vendor/stdlib/src/Category/Monad.agda
  32. +59 −0 vendor/stdlib/src/Category/Monad/Continuation.agda
  33. +16 −0 vendor/stdlib/src/Category/Monad/Identity.agda
  34. +50 −0 vendor/stdlib/src/Category/Monad/Indexed.agda
  35. +89 −0 vendor/stdlib/src/Category/Monad/Partiality.agda
  36. +111 −0 vendor/stdlib/src/Category/Monad/State.agda
  37. +25 −0 vendor/stdlib/src/Coinduction.agda
  38. +302 −0 vendor/stdlib/src/Data/AVL.agda
  39. +84 −0 vendor/stdlib/src/Data/AVL/IndexedMap.agda
  40. +56 −0 vendor/stdlib/src/Data/AVL/Sets.agda
  41. +356 −0 vendor/stdlib/src/Data/Bin.agda
  42. +83 −0 vendor/stdlib/src/Data/Bool.agda
  43. +313 −0 vendor/stdlib/src/Data/Bool/Properties.agda
  44. +12 −0 vendor/stdlib/src/Data/Bool/Show.agda
  45. +72 −0 vendor/stdlib/src/Data/BoundedVec.agda
  46. +39 −0 vendor/stdlib/src/Data/BoundedVec/Inefficient.agda
  47. +49 −0 vendor/stdlib/src/Data/Char.agda
  48. +40 −0 vendor/stdlib/src/Data/Cofin.agda
  49. +183 −0 vendor/stdlib/src/Data/Colist.agda
  50. +31 −0 vendor/stdlib/src/Data/Conat.agda
  51. +164 −0 vendor/stdlib/src/Data/Covec.agda
  52. +57 −0 vendor/stdlib/src/Data/DifferenceList.agda
  53. +34 −0 vendor/stdlib/src/Data/DifferenceNat.agda
  54. +49 −0 vendor/stdlib/src/Data/DifferenceVec.agda
  55. +119 −0 vendor/stdlib/src/Data/Digit.agda
  56. +10 −0 vendor/stdlib/src/Data/Empty.agda
  57. +7 −0 vendor/stdlib/src/Data/Empty1.agda
  58. +184 −0 vendor/stdlib/src/Data/Fin.agda
  59. +152 −0 vendor/stdlib/src/Data/Fin/Dec.agda
  60. +168 −0 vendor/stdlib/src/Data/Fin/Props.agda
  61. +62 −0 vendor/stdlib/src/Data/Fin/Subset.agda
  62. +61 −0 vendor/stdlib/src/Data/Fin/Subset/Props.agda
  63. +174 −0 vendor/stdlib/src/Data/Fin/Substitution.agda
  64. +90 −0 vendor/stdlib/src/Data/Fin/Substitution/Example.agda
  65. +512 −0 vendor/stdlib/src/Data/Fin/Substitution/Lemmas.agda
  66. +42 −0 vendor/stdlib/src/Data/Fin/Substitution/List.agda
  67. +106 −0 vendor/stdlib/src/Data/Function.agda
  68. +316 −0 vendor/stdlib/src/Data/Graph/Acyclic.agda
  69. +267 −0 vendor/stdlib/src/Data/Integer.agda
  70. +31 −0 vendor/stdlib/src/Data/Integer/Divisibility.agda
  71. +87 −0 vendor/stdlib/src/Data/Integer/Properties.agda
  72. +295 −0 vendor/stdlib/src/Data/List.agda
  73. +49 −0 vendor/stdlib/src/Data/List/All.agda
  74. +57 −0 vendor/stdlib/src/Data/List/All/Properties.agda
  75. +191 −0 vendor/stdlib/src/Data/List/Any.agda
  76. +459 −0 vendor/stdlib/src/Data/List/Any/Properties.agda
  77. +236 −0 vendor/stdlib/src/Data/List/Countdown.agda
  78. +88 −0 vendor/stdlib/src/Data/List/Equality.agda
  79. +151 −0 vendor/stdlib/src/Data/List/NonEmpty.agda
  80. +47 −0 vendor/stdlib/src/Data/List/NonEmpty/Properties.agda
  81. +247 −0 vendor/stdlib/src/Data/List/Properties.agda
  82. +44 −0 vendor/stdlib/src/Data/List1.agda
  83. +83 −0 vendor/stdlib/src/Data/Map.agda
  84. +133 −0 vendor/stdlib/src/Data/Maybe.agda
  85. +11 −0 vendor/stdlib/src/Data/Maybe/Core.agda
  86. +235 −0 vendor/stdlib/src/Data/Nat.agda
  87. +136 −0 vendor/stdlib/src/Data/Nat/Coprimality.agda
  88. +114 −0 vendor/stdlib/src/Data/Nat/DivMod.agda
  89. +205 −0 vendor/stdlib/src/Data/Nat/Divisibility.agda
  90. +187 −0 vendor/stdlib/src/Data/Nat/GCD.agda
  91. +168 −0 vendor/stdlib/src/Data/Nat/GCD/Lemmas.agda
  92. +125 −0 vendor/stdlib/src/Data/Nat/LCM.agda
  93. +660 −0 vendor/stdlib/src/Data/Nat/Properties.agda
  94. +31 −0 vendor/stdlib/src/Data/Nat/Show.agda
  95. +79 −0 vendor/stdlib/src/Data/Product.agda
  96. +61 −0 vendor/stdlib/src/Data/Product/Record.agda
  97. +79 −0 vendor/stdlib/src/Data/Product1.agda
  98. +109 −0 vendor/stdlib/src/Data/Rational.agda
  99. +94 −0 vendor/stdlib/src/Data/Sets.agda
  100. +37 −0 vendor/stdlib/src/Data/Sign.agda
  101. +24 −0 vendor/stdlib/src/Data/Sign/Properties.agda
  102. +135 −0 vendor/stdlib/src/Data/Star.agda
  103. +62 −0 vendor/stdlib/src/Data/Star/BoundedVec.agda
  104. +87 −0 vendor/stdlib/src/Data/Star/Decoration.agda
  105. +41 −0 vendor/stdlib/src/Data/Star/Environment.agda
  106. +23 −0 vendor/stdlib/src/Data/Star/Fin.agda
  107. +30 −0 vendor/stdlib/src/Data/Star/List.agda
  108. +54 −0 vendor/stdlib/src/Data/Star/Nat.agda
  109. +87 −0 vendor/stdlib/src/Data/Star/Pointer.agda
  110. +89 −0 vendor/stdlib/src/Data/Star/Properties.agda
  111. +63 −0 vendor/stdlib/src/Data/Star/Vec.agda
  112. +122 −0 vendor/stdlib/src/Data/Stream.agda
  113. +76 −0 vendor/stdlib/src/Data/String.agda
  114. +45 −0 vendor/stdlib/src/Data/Sum.agda
  115. +76 −0 vendor/stdlib/src/Data/Unit.agda
  116. +7 −0 vendor/stdlib/src/Data/Unit1.agda
  117. +196 −0 vendor/stdlib/src/Data/Vec.agda
  118. +89 −0 vendor/stdlib/src/Data/Vec/Equality.agda
  119. +98 −0 vendor/stdlib/src/Data/Vec/N-ary.agda
  120. +84 −0 vendor/stdlib/src/Data/Vec/N-ary1.agda
  121. +138 −0 vendor/stdlib/src/Data/Vec/Properties.agda
  122. +39 −0 vendor/stdlib/src/Data/Vec1.agda
  123. +36 −0 vendor/stdlib/src/Foreign/Haskell.agda
  124. +99 −0 vendor/stdlib/src/IO.agda
  125. +46 −0 vendor/stdlib/src/IO/Primitive.agda
  126. +49 −0 vendor/stdlib/src/Induction.agda
  127. +61 −0 vendor/stdlib/src/Induction/Lexicographic.agda
  128. +109 −0 vendor/stdlib/src/Induction/Nat.agda
  129. +45 −0 vendor/stdlib/src/Induction/WellFounded.agda
  130. +47 −0 vendor/stdlib/src/Induction1.agda
  131. +29 −0 vendor/stdlib/src/Induction1/Nat.agda
  132. +47 −0 vendor/stdlib/src/Induction1/WellFounded.agda
  133. +266 −0 vendor/stdlib/src/Relation/Binary.agda
  134. +120 −0 vendor/stdlib/src/Relation/Binary/Consequences.agda
  135. +16 −0 vendor/stdlib/src/Relation/Binary/Consequences/Core.agda
  136. +159 −0 vendor/stdlib/src/Relation/Binary/Core.agda
  137. +29 −0 vendor/stdlib/src/Relation/Binary/EqReasoning.agda
  138. +183 −0 vendor/stdlib/src/Relation/Binary/Flip.agda
  139. +68 −0 vendor/stdlib/src/Relation/Binary/FunctionSetoid.agda
  140. +170 −0 vendor/stdlib/src/Relation/Binary/HeterogeneousEquality.agda
  141. +76 −0 vendor/stdlib/src/Relation/Binary/NonStrictToStrict.agda
  142. +124 −0 vendor/stdlib/src/Relation/Binary/On.agda
  143. +39 −0 vendor/stdlib/src/Relation/Binary/OrderMorphism.agda
  144. +11 −0 vendor/stdlib/src/Relation/Binary/PartialOrderReasoning.agda
  145. +51 −0 vendor/stdlib/src/Relation/Binary/PreorderReasoning.agda
  146. +166 −0 vendor/stdlib/src/Relation/Binary/Product/NonStrictLex.agda
  147. +213 −0 vendor/stdlib/src/Relation/Binary/Product/Pointwise.agda
  148. +248 −0 vendor/stdlib/src/Relation/Binary/Product/StrictLex.agda
  149. +113 −0 vendor/stdlib/src/Relation/Binary/PropositionalEquality.agda
  150. +33 −0 vendor/stdlib/src/Relation/Binary/PropositionalEquality/Core.agda
  151. +50 −0 vendor/stdlib/src/Relation/Binary/PropositionalEquality1.agda
  152. +23 −0 vendor/stdlib/src/Relation/Binary/Props/DecTotalOrder.agda
  153. +26 −0 vendor/stdlib/src/Relation/Binary/Props/Poset.agda
  154. +32 −0 vendor/stdlib/src/Relation/Binary/Props/StrictPartialOrder.agda
  155. +32 −0 vendor/stdlib/src/Relation/Binary/Props/StrictTotalOrder.agda
  156. +19 −0 vendor/stdlib/src/Relation/Binary/Props/TotalOrder.agda
  157. +82 −0 vendor/stdlib/src/Relation/Binary/Reflection.agda
  158. +29 −0 vendor/stdlib/src/Relation/Binary/Simple.agda
  159. +13 −0 vendor/stdlib/src/Relation/Binary/StrictPartialOrderReasoning.agda
  160. +100 −0 vendor/stdlib/src/Relation/Binary/StrictToNonStrict.agda
  161. +349 −0 vendor/stdlib/src/Relation/Binary/Sum.agda
  162. +68 −0 vendor/stdlib/src/Relation/Nullary.agda
  163. +22 −0 vendor/stdlib/src/Relation/Nullary/Core.agda
  164. +40 −0 vendor/stdlib/src/Relation/Nullary/Decidable.agda
  165. +99 −0 vendor/stdlib/src/Relation/Nullary/Negation.agda
  166. +16 −0 vendor/stdlib/src/Relation/Nullary/Product.agda
  167. +24 −0 vendor/stdlib/src/Relation/Nullary/Sum.agda
  168. +130 −0 vendor/stdlib/src/Relation/Nullary/Universe.agda
  169. +129 −0 vendor/stdlib/src/Relation/Unary.agda
  170. +52 −0 vendor/stdlib/src/Relation/Unary1.agda
  171. +14 −0 vendor/stdlib/src/Size.agda
View
@@ -0,0 +1,5 @@
+\.l?agda\.el$
+\.agdai$
+(^|/)MAlonzo($|/)
+^html($|/)
+^Everything\.agda$
@@ -0,0 +1,27 @@
+-- | This module extracts all the non-ASCII characters used by the
+-- library code (along with how many times they are used).
+--
+-- The implementation relies on the utf8-string and FileManip
+-- libraries which are available from Hackage.
+
+module AllNonAsciiChars where
+
+import qualified Data.List as L
+import Data.Char
+import Data.Function
+import Control.Applicative
+import System.IO.UTF8 as U
+import System.FilePath.Find
+
+main :: IO ()
+main = do
+ agdaFiles <- find always
+ (extension ~~? ".agda" ||? extension ~~? ".lagda")
+ "src"
+ nonAsciiChars <-
+ filter (not . isAscii) . concat <$> mapM U.readFile agdaFiles
+ let table = reverse $
+ L.sortBy (compare `on` snd) $
+ map (\cs -> (head cs, length cs)) $
+ L.group $ L.sort $ nonAsciiChars
+ mapM_ (\(c, count) -> U.putStrLn (c : ": " ++ show count)) table
Oops, something went wrong.

0 comments on commit b72c796

Please sign in to comment.