@@ -12,7 +12,7 @@ getProof (a ** v) = v
1212
1313FalseElim : _|_ -> a
1414
15−-- For rewrite tactic
15+-- ------------------------------------------------------ [ For rewrite tactic ]
1616replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
1717replace refl prf = prf
1818
@@ -42,36 +42,45 @@ public %assert_total -- reduces at compile time, use with extreme care!
4242really_believe_me : a -> b
4343really_believe_me x = prim__believe_me _ _ x
4444
45+-- ---------------------------------------------------------------- [ Builtins ]
4546namespace Builtins {
4647
4748Not : Type -> Type
4849Not a = a -> _|_
4950
51+-- | Identity function.
5052id : a -> a
5153id x = x
5254
55+-- | Manually assign a type to an expression.
5356the : (a : Type) -> a -> a
5457the _ = id
5558
59+-- | Constant function.
5660const : a -> b -> a
5761const x _ = x
5862
63+-- | Return the first element of a pair.
5964fst : (s, t) -> s
6065fst (x, y) = x
6166
67+-- | Return the second element of a pair.
6268snd : (a, b) -> b
6369snd (x, y) = y
6470
6571infixl 9 .
6672
73+-- | Function composition
6774(.) : (b -> c) -> (a -> b) -> a -> c
6875(.) f g x = f (g x)
6976
77+-- | Takes in the first two arguments in reverse order.
7078flip : (a -> b -> c) -> b -> a -> c
7179flip f x y = f y x
7280
7381infixr 1 $
7482
83+-- | Function application.
7584($) : (a -> b) -> a -> b
7685f $ a = f a
7786
@@ -82,39 +91,47 @@ data Dec : Type -> Type where
8291 Yes : {A : Type} -> A -> Dec A
8392 No : {A : Type} -> (A -> _|_) -> Dec A
8493
94+-- | Boolean Data Type
8595data Bool = False | True
8696
97+-- | Boolean elimination
8798boolElim : Bool -> |(t : a) -> |(f : a) -> a
8899boolElim True t e = t
89100boolElim False t e = e
90101
102+-- | Defines a predicate on Bool which guarantees that the value is true.
91103data so : Bool -> Type where oh : so True
92104
105+-- Syntaxtic sugar for boolean elimination.
93106syntax if [test] then [t] else [e] = boolElim test t e
94107syntax [test] "?" [t] ":" [e] = if test then t else e
95108
109+-- Boolean Operator Precedence
96110infixl 4 &&, ||
97111
112+-- | Boolean OR
98113(||) : Bool -> Bool -> Bool
99114(||) False x = x
100115(||) True _ = True
101116
117+-- | Boolean AND
102118(&&) : Bool -> Bool -> Bool
103119(&&) True x = x
104120(&&) False _ = False
105121
122+-- | Boolean NOT
106123not : Bool -> Bool
107124not True = False
108125not False = True
109126
127+-- Numerical Operator Precedence
110128infixl 5 ==, /=
111129infixl 6 <, <=, >, >=
112130infixl 7 <<, >>
113131infixl 8 +,-,++
114132infixl 9 *,/
115133
116−--- Numeric operators
117−
134+-- ------------------------------------------------------- [ Numeric Operators ]
118135intToBool : Int -> Bool
119136intToBool 0 = False
120137intToBool x = True
@@ -122,6 +139,7 @@ intToBool x = True
122139boolOp : (a -> a -> Int) -> a -> a -> Bool
123140boolOp op x y = intToBool (op x y)
124141
142+-- | The Eq class defines inequality and equality.
125143class Eq a where
126144 (==) : a -> a -> Bool
127145 (/=) : a -> a -> Bool
@@ -162,6 +180,7 @@ instance Eq Ordering where
162180 GT == GT = True
163181 _ == _ = False
164182
183+-- | The Ord class defines comparison operations on ordered data types.
165184class Eq a => Ord a where
166185 compare : a -> a -> Ordering
167186
@@ -224,13 +243,14 @@ instance (Ord a, Ord b) => Ord (a, b) where
224243 then compare xl yl
225244 else compare xr yr
226245
227−
246+-- | The Num class defines basic numerical arithmetic.
228247class Num a where
229248 (+) : a -> a -> a
230249 (-) : a -> a -> a
231250 (*) : a -> a -> a
232−
251+ -- | Absolute value
233252 abs : a -> a
253+ -- | Conversion from Integer.
234254 fromInteger : Integer -> a
235255
236256instance Num Integer where
@@ -334,38 +354,45 @@ instance Ord Bits64 where
334354 else if l > r then GT
335355 else EQ
336356
357+-- | Integer division.
337358partial
338359div : Integer -> Integer -> Integer
339360div = prim__sdivBigInt
340361
362+-- | Integer modulus.
341363partial
342364mod : Integer -> Integer -> Integer
343365mod = prim__sremBigInt
344366
345−
367+-- | Fractional division of two Floats.
346368(/) : Float -> Float -> Float
347369(/) = prim__divFloat
348370
349−--- string operators
350−
371+-- -------------------------------------------------------- [ String Operators ]
372+-- | Appends two strings together.
351373(++) : String -> String -> String
352374(++) = prim__concat
353375
376+-- | Returns the first character in the specified string.
354377partial
355378strHead : String -> Char
356379strHead = prim__strHead
357380
381+-- | Returns the characters specified after the head of the string.
358382partial
359383strTail : String -> String
360384strTail = prim__strTail
361385
386+-- | Adds a character to the from of the specified string.
362387strCons : Char -> String -> String
363388strCons = prim__strCons
364389
390+-- | Returns the nth character (starting from 0) of the specified string.
365391partial
366392strIndex : String -> Int -> Char
367393strIndex = prim__strIndex
368394
395+-- | Reverses the elements within a String.
369396reverse : String -> String
370397reverse = prim__strRev
371398