diff --git a/lib/Agda.Builtin.Bool.html b/lib/Agda.Builtin.Bool.html deleted file mode 100644 index 63da33b2..00000000 --- a/lib/Agda.Builtin.Bool.html +++ /dev/null @@ -1,17 +0,0 @@ - -Agda.Builtin.Bool
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Bool where
-
-data Bool : Set where
-  false true : Bool
-
-{-# BUILTIN BOOL  Bool  #-}
-{-# BUILTIN FALSE false #-}
-{-# BUILTIN TRUE  true  #-}
-
-{-# COMPILE JS Bool  = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
-{-# COMPILE JS false = false #-}
-{-# COMPILE JS true  = true  #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Char.html b/lib/Agda.Builtin.Char.html deleted file mode 100644 index ec85da80..00000000 --- a/lib/Agda.Builtin.Char.html +++ /dev/null @@ -1,20 +0,0 @@ - -Agda.Builtin.Char
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Char where
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Bool
-
-postulate Char : Set
-{-# BUILTIN CHAR Char #-}
-
-primitive
-  primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii
-    primIsLatin1 primIsPrint primIsHexDigit : Char → Bool
-  primToUpper primToLower : Char → Char
-  primCharToNat : Char → Nat
-  primNatToChar : Nat → Char
-  primCharEquality : Char → Char → Bool
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Equality.html b/lib/Agda.Builtin.Equality.html deleted file mode 100644 index d686af44..00000000 --- a/lib/Agda.Builtin.Equality.html +++ /dev/null @@ -1,11 +0,0 @@ - -Agda.Builtin.Equality
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Equality where
-
-infix 4 _≡_
-data _≡_ {a} {A : Set a} (x : A) : A → Set a where
-  instance refl : x ≡ x
-
-{-# BUILTIN EQUALITY _≡_ #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Float.html b/lib/Agda.Builtin.Float.html deleted file mode 100644 index 34c1c528..00000000 --- a/lib/Agda.Builtin.Float.html +++ /dev/null @@ -1,211 +0,0 @@ - -Agda.Builtin.Float
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Float where
-
-open import Agda.Builtin.Bool
-open import Agda.Builtin.Int
-open import Agda.Builtin.Maybe
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Sigma
-open import Agda.Builtin.String
-open import Agda.Builtin.Word
-
-postulate Float : Set
-{-# BUILTIN FLOAT Float #-}
-
-primitive
-  -- Relations
-  primFloatInequality        : Float → Float → Bool
-  primFloatEquality          : Float → Float → Bool
-  primFloatLess              : Float → Float → Bool
-  primFloatIsInfinite        : Float → Bool
-  primFloatIsNaN             : Float → Bool
-  primFloatIsNegativeZero    : Float → Bool
-  primFloatIsSafeInteger     : Float → Bool
-  -- Conversions
-  primFloatToWord64          : Float → Maybe Word64
-  primNatToFloat             : Nat → Float
-  primIntToFloat             : Int → Float
-  primFloatRound             : Float → Maybe Int
-  primFloatFloor             : Float → Maybe Int
-  primFloatCeiling           : Float → Maybe Int
-  primFloatToRatio           : Float → (Σ Int λ _ → Int)
-  primRatioToFloat           : Int → Int → Float
-  primFloatDecode            : Float → Maybe (Σ Int λ _ → Int)
-  primFloatEncode            : Int → Int → Maybe Float
-  primShowFloat              : Float → String
-  -- Operations
-  primFloatPlus              : Float → Float → Float
-  primFloatMinus             : Float → Float → Float
-  primFloatTimes             : Float → Float → Float
-  primFloatDiv               : Float → Float → Float
-  primFloatPow               : Float → Float → Float
-  primFloatNegate            : Float → Float
-  primFloatSqrt              : Float → Float
-  primFloatExp               : Float → Float
-  primFloatLog               : Float → Float
-  primFloatSin               : Float → Float
-  primFloatCos               : Float → Float
-  primFloatTan               : Float → Float
-  primFloatASin              : Float → Float
-  primFloatACos              : Float → Float
-  primFloatATan              : Float → Float
-  primFloatATan2             : Float → Float → Float
-  primFloatSinh              : Float → Float
-  primFloatCosh              : Float → Float
-  primFloatTanh              : Float → Float
-  primFloatASinh             : Float → Float
-  primFloatACosh             : Float → Float
-  primFloatATanh             : Float → Float
-
-{-# COMPILE JS
-    primFloatRound = function(x) {
-        x = agdaRTS._primFloatRound(x);
-        if (x === null) {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
-        }
-        else {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
-        }
-    };
-#-}
-{-# COMPILE JS
-    primFloatFloor = function(x) {
-        x = agdaRTS._primFloatFloor(x);
-        if (x === null) {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
-        }
-        else {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
-        }
-    };
-#-}
-{-# COMPILE JS
-    primFloatCeiling = function(x) {
-        x = agdaRTS._primFloatCeiling(x);
-        if (x === null) {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
-        }
-        else {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
-        }
-    };
-#-}
-{-# COMPILE JS
-    primFloatToRatio = function(x) {
-        x = agdaRTS._primFloatToRatio(x);
-        return z_jAgda_Agda_Builtin_Sigma["_,_"](x.numerator)(x.denominator);
-    };
-#-}
-{-# COMPILE JS
-    primFloatDecode = function(x) {
-        x = agdaRTS._primFloatDecode(x);
-        if (x === null) {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
-        }
-        else {
-            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](
-                z_jAgda_Agda_Builtin_Sigma["_,_"](x.mantissa)(x.exponent));
-        }
-    };
-#-}
-{-# COMPILE JS
-    primFloatEncode = function(x) {
-        return function (y) {
-            x = agdaRTS.uprimFloatEncode(x, y);
-            if (x === null) {
-                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
-            }
-            else {
-                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
-            }
-        }
-    };
-#-}
-
-primFloatNumericalEquality = primFloatEquality
-{-# WARNING_ON_USAGE primFloatNumericalEquality
-"Warning: primFloatNumericalEquality was deprecated in Agda v2.6.2.
-Please use primFloatEquality instead."
-#-}
-
-primFloatNumericalLess = primFloatLess
-{-# WARNING_ON_USAGE primFloatNumericalLess
-"Warning: primFloatNumericalLess was deprecated in Agda v2.6.2.
-Please use primFloatLess instead."
-#-}
-
-primRound = primFloatRound
-{-# WARNING_ON_USAGE primRound
-"Warning: primRound was deprecated in Agda v2.6.2.
-Please use primFloatRound instead."
-#-}
-
-primFloor = primFloatFloor
-{-# WARNING_ON_USAGE primFloor
-"Warning: primFloor was deprecated in Agda v2.6.2.
-Please use primFloatFloor instead."
-#-}
-
-primCeiling = primFloatCeiling
-{-# WARNING_ON_USAGE primCeiling
-"Warning: primCeiling was deprecated in Agda v2.6.2.
-Please use primFloatCeiling instead."
-#-}
-
-primExp = primFloatExp
-{-# WARNING_ON_USAGE primExp
-"Warning: primExp was deprecated in Agda v2.6.2.
-Please use primFloatExp instead."
-#-}
-
-primLog = primFloatLog
-{-# WARNING_ON_USAGE primLog
-"Warning: primLog was deprecated in Agda v2.6.2.
-Please use primFloatLog instead."
-#-}
-
-primSin = primFloatSin
-{-# WARNING_ON_USAGE primSin
-"Warning: primSin was deprecated in Agda v2.6.2.
-Please use primFloatSin instead."
-#-}
-
-primCos = primFloatCos
-{-# WARNING_ON_USAGE primCos
-"Warning: primCos was deprecated in Agda v2.6.2.
-Please use primFloatCos instead."
-#-}
-
-primTan = primFloatTan
-{-# WARNING_ON_USAGE primTan
-"Warning: primTan was deprecated in Agda v2.6.2.
-Please use primFloatTan instead."
-#-}
-
-primASin = primFloatASin
-{-# WARNING_ON_USAGE primASin
-"Warning: primASin was deprecated in Agda v2.6.2.
-Please use primFloatASin instead."
-#-}
-
-
-primACos = primFloatACos
-{-# WARNING_ON_USAGE primACos
-"Warning: primACos was deprecated in Agda v2.6.2.
-Please use primFloatACos instead."
-#-}
-
-primATan = primFloatATan
-{-# WARNING_ON_USAGE primATan
-"Warning: primATan was deprecated in Agda v2.6.2.
-Please use primFloatATan instead."
-#-}
-
-primATan2 = primFloatATan2
-{-# WARNING_ON_USAGE primATan2
-"Warning: primATan2 was deprecated in Agda v2.6.2.
-Please use primFloatATan2 instead."
-#-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromNat.html b/lib/Agda.Builtin.FromNat.html deleted file mode 100644 index acfa25ae..00000000 --- a/lib/Agda.Builtin.FromNat.html +++ /dev/null @@ -1,18 +0,0 @@ - -Agda.Builtin.FromNat
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.FromNat where
-
-open import Agda.Primitive
-open import Agda.Builtin.Nat
-
-record Number {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : Nat → Set a
-    fromNat : ∀ n → {{_ : Constraint n}} → A
-
-open Number {{...}} public using (fromNat)
-
-{-# BUILTIN FROMNAT fromNat #-}
-{-# DISPLAY Number.fromNat _ n = fromNat n #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromNeg.html b/lib/Agda.Builtin.FromNeg.html deleted file mode 100644 index 6253b020..00000000 --- a/lib/Agda.Builtin.FromNeg.html +++ /dev/null @@ -1,18 +0,0 @@ - -Agda.Builtin.FromNeg
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.FromNeg where
-
-open import Agda.Primitive
-open import Agda.Builtin.Nat
-
-record Negative {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : Nat → Set a
-    fromNeg : ∀ n → {{_ : Constraint n}} → A
-
-open Negative {{...}} public using (fromNeg)
-
-{-# BUILTIN FROMNEG fromNeg #-}
-{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromString.html b/lib/Agda.Builtin.FromString.html deleted file mode 100644 index 0b9dffdc..00000000 --- a/lib/Agda.Builtin.FromString.html +++ /dev/null @@ -1,18 +0,0 @@ - -Agda.Builtin.FromString
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.FromString where
-
-open import Agda.Primitive
-open import Agda.Builtin.String
-
-record IsString {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : String → Set a
-    fromString : (s : String) {{_ : Constraint s}} → A
-
-open IsString {{...}} public using (fromString)
-
-{-# BUILTIN FROMSTRING fromString #-}
-{-# DISPLAY IsString.fromString _ s = fromString s #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Int.html b/lib/Agda.Builtin.Int.html deleted file mode 100644 index 775af21f..00000000 --- a/lib/Agda.Builtin.Int.html +++ /dev/null @@ -1,20 +0,0 @@ - -Agda.Builtin.Int
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Int where
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.String
-
-infix 8 pos  -- Standard library uses this as +_
-
-data Int : Set where
-  pos    : (n : Nat) → Int
-  negsuc : (n : Nat) → Int
-
-{-# BUILTIN INTEGER       Int    #-}
-{-# BUILTIN INTEGERPOS    pos    #-}
-{-# BUILTIN INTEGERNEGSUC negsuc #-}
-
-primitive primShowInteger : Int → String
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.List.html b/lib/Agda.Builtin.List.html deleted file mode 100644 index add6de61..00000000 --- a/lib/Agda.Builtin.List.html +++ /dev/null @@ -1,18 +0,0 @@ - -Agda.Builtin.List
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.List where
-
-infixr 5 _∷_
-data List {a} (A : Set a) : Set a where
-  []  : List A
-  _∷_ : (x : A) (xs : List A) → List A
-
-{-# BUILTIN LIST List #-}
-
-{-# COMPILE JS  List = function(x,v) {
-  if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
-} #-}
-{-# COMPILE JS [] = Array() #-}
-{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Maybe.html b/lib/Agda.Builtin.Maybe.html deleted file mode 100644 index 76d37bd3..00000000 --- a/lib/Agda.Builtin.Maybe.html +++ /dev/null @@ -1,11 +0,0 @@ - -Agda.Builtin.Maybe
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Maybe where
-
-data Maybe {a} (A : Set a) : Set a where
-  just : A → Maybe A
-  nothing : Maybe A
-
-{-# BUILTIN MAYBE Maybe #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Nat.html b/lib/Agda.Builtin.Nat.html deleted file mode 100644 index 6ccb7bda..00000000 --- a/lib/Agda.Builtin.Nat.html +++ /dev/null @@ -1,136 +0,0 @@ - -Agda.Builtin.Nat
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Nat where
-
-open import Agda.Builtin.Bool
-
-data Nat : Set where
-  zero : Nat
-  suc  : (n : Nat) → Nat
-
-{-# BUILTIN NATURAL Nat #-}
-
-infix  4 _==_ _<_
-infixl 6 _+_ _-_
-infixl 7 _*_
-
-_+_ : Nat → Nat → Nat
-zero  + m = m
-suc n + m = suc (n + m)
-
-{-# BUILTIN NATPLUS _+_ #-}
-
-_-_ : Nat → Nat → Nat
-n     - zero = n
-zero  - suc m = zero
-suc n - suc m = n - m
-
-{-# BUILTIN NATMINUS _-_ #-}
-
-_*_ : Nat → Nat → Nat
-zero  * m = zero
-suc n * m = m + n * m
-
-{-# BUILTIN NATTIMES _*_ #-}
-
-_==_ : Nat → Nat → Bool
-zero  == zero  = true
-suc n == suc m = n == m
-_     == _     = false
-
-{-# BUILTIN NATEQUALS _==_ #-}
-
-_<_ : Nat → Nat → Bool
-_     < zero  = false
-zero  < suc _ = true
-suc n < suc m = n < m
-
-{-# BUILTIN NATLESS _<_ #-}
-
--- Helper function  div-helper  for Euclidean division.
----------------------------------------------------------------------------
---
--- div-helper computes n / 1+m via iteration on n.
---
---   n div (suc m) = div-helper 0 m n m
---
--- The state of the iterator has two accumulator variables:
---
---   k: The quotient, returned once n=0.  Initialized to 0.
---
---   j: A counter, initialized to the divisor m, decreased on each iteration step.
---      Once it reaches 0, the quotient k is increased and j reset to m,
---      starting the next countdown.
---
--- Under the precondition j ≤ m, the invariant is
---
---   div-helper k m n j = k + (n + m - j) div (1 + m)
-
-div-helper : (k m n j : Nat) → Nat
-div-helper k m  zero    j      = k
-div-helper k m (suc n)  zero   = div-helper (suc k) m n m
-div-helper k m (suc n) (suc j) = div-helper k       m n j
-
-{-# BUILTIN NATDIVSUCAUX div-helper #-}
-
--- Proof of the invariant by induction on n.
---
---   clause 1: div-helper k m 0 j
---           = k                                        by definition
---           = k + (0 + m - j) div (1 + m)              since m - j < 1 + m
---
---   clause 2: div-helper k m (1 + n) 0
---           = div-helper (1 + k) m n m                 by definition
---           = 1 + k + (n + m - m) div (1 + m)          by induction hypothesis
---           = 1 + k +          n  div (1 + m)          by simplification
---           = k +   (n + (1 + m)) div (1 + m)          by expansion
---           = k + (1 + n + m - 0) div (1 + m)          by expansion
---
---   clause 3: div-helper k m (1 + n) (1 + j)
---           = div-helper k m n j                       by definition
---           = k + (n + m - j) div (1 + m)              by induction hypothesis
---           = k + ((1 + n) + m - (1 + j)) div (1 + m)  by expansion
---
--- Q.e.d.
-
--- Helper function  mod-helper  for the remainder computation.
----------------------------------------------------------------------------
---
--- (Analogous to div-helper.)
---
--- mod-helper computes n % 1+m via iteration on n.
---
---   n mod (suc m) = mod-helper 0 m n m
---
--- The invariant is:
---
---   m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).
-
-mod-helper : (k m n j : Nat) → Nat
-mod-helper k m  zero    j      = k
-mod-helper k m (suc n)  zero   = mod-helper 0       m n m
-mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
-
-{-# BUILTIN NATMODSUCAUX mod-helper #-}
-
--- Proof of the invariant by induction on n.
---
---   clause 1: mod-helper k m 0 j
---           = k                               by definition
---           = (0 + k) mod (1 + m)             since m = k + j, thus k < m
---
---   clause 2: mod-helper k m (1 + n) 0
---           = mod-helper 0 m n m              by definition
---           = (n + 0)       mod (1 + m)       by induction hypothesis
---           = (n + (1 + m)) mod (1 + m)       by expansion
---           = (1 + n) + k)  mod (1 + m)       since k = m (as l = 0)
---
---   clause 3: mod-helper k m (1 + n) (1 + j)
---           = mod-helper (1 + k) m n j        by definition
---           = (n + (1 + k)) mod (1 + m)       by induction hypothesis
---           = ((1 + n) + k) mod (1 + m)       by commutativity
---
--- Q.e.d.
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Reflection.html b/lib/Agda.Builtin.Reflection.html deleted file mode 100644 index e516a77e..00000000 --- a/lib/Agda.Builtin.Reflection.html +++ /dev/null @@ -1,472 +0,0 @@ - -Agda.Builtin.Reflection
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Reflection where
-
-open import Agda.Builtin.Unit
-open import Agda.Builtin.Bool
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Word
-open import Agda.Builtin.List
-open import Agda.Builtin.String
-open import Agda.Builtin.Char
-open import Agda.Builtin.Float
-open import Agda.Builtin.Int
-open import Agda.Builtin.Sigma
-open import Agda.Primitive
-
--- Names --
-
-postulate Name : Set
-{-# BUILTIN QNAME Name #-}
-
-primitive
-  primQNameEquality : Name → Name → Bool
-  primQNameLess     : Name → Name → Bool
-  primShowQName     : Name → String
-
--- Fixity --
-
-data Associativity : Set where
-  left-assoc  : Associativity
-  right-assoc : Associativity
-  non-assoc   : Associativity
-
-data Precedence : Set where
-  related   : Float → Precedence
-  unrelated : Precedence
-
-data Fixity : Set where
-  fixity : Associativity → Precedence → Fixity
-
-{-# BUILTIN ASSOC      Associativity #-}
-{-# BUILTIN ASSOCLEFT  left-assoc    #-}
-{-# BUILTIN ASSOCRIGHT right-assoc   #-}
-{-# BUILTIN ASSOCNON   non-assoc     #-}
-
-{-# BUILTIN PRECEDENCE    Precedence #-}
-{-# BUILTIN PRECRELATED   related    #-}
-{-# BUILTIN PRECUNRELATED unrelated  #-}
-
-{-# BUILTIN FIXITY       Fixity #-}
-{-# BUILTIN FIXITYFIXITY fixity #-}
-
-{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-}
-{-# COMPILE GHC Precedence    = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-}
-{-# COMPILE GHC Fixity        = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-}
-
-{-# COMPILE JS Associativity  = function (x,v) { return v[x](); } #-}
-{-# COMPILE JS left-assoc     = "left-assoc"  #-}
-{-# COMPILE JS right-assoc    = "right-assoc" #-}
-{-# COMPILE JS non-assoc      = "non-assoc"   #-}
-
-{-# COMPILE JS Precedence     =
-  function (x,v) {
-    if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-}
-{-# COMPILE JS related        = function(x) { return x; } #-}
-{-# COMPILE JS unrelated      = "unrelated"               #-}
-
-{-# COMPILE JS Fixity         = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-}
-{-# COMPILE JS fixity         = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-}
-
-primitive
-  primQNameFixity : Name → Fixity
-  primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)
-
--- Metavariables --
-
-postulate Meta : Set
-{-# BUILTIN AGDAMETA Meta #-}
-
-primitive
-  primMetaEquality : Meta → Meta → Bool
-  primMetaLess     : Meta → Meta → Bool
-  primShowMeta     : Meta → String
-  primMetaToNat    : Meta → Nat
-
--- Arguments --
-
--- Arguments can be (visible), {hidden}, or {{instance}}.
-data Visibility : Set where
-  visible hidden instance′ : Visibility
-
-{-# BUILTIN HIDING   Visibility #-}
-{-# BUILTIN VISIBLE  visible    #-}
-{-# BUILTIN HIDDEN   hidden     #-}
-{-# BUILTIN INSTANCE instance′  #-}
-
--- Arguments can be relevant or irrelevant.
-data Relevance : Set where
-  relevant irrelevant : Relevance
-
-{-# BUILTIN RELEVANCE  Relevance  #-}
-{-# BUILTIN RELEVANT   relevant   #-}
-{-# BUILTIN IRRELEVANT irrelevant #-}
-
--- Arguments also have a quantity.
-data Quantity : Set where
-  quantity-0 quantity-ω : Quantity
-
-{-# BUILTIN QUANTITY   Quantity   #-}
-{-# BUILTIN QUANTITY-0 quantity-0 #-}
-{-# BUILTIN QUANTITY-ω quantity-ω #-}
-
--- Relevance and quantity are combined into a modality.
-data Modality : Set where
-  modality : (r : Relevance) (q : Quantity) → Modality
-
-{-# BUILTIN MODALITY             Modality #-}
-{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
-
-data ArgInfo : Set where
-  arg-info : (v : Visibility) (m : Modality) → ArgInfo
-
-data Arg {a} (A : Set a) : Set a where
-  arg : (i : ArgInfo) (x : A) → Arg A
-
-{-# BUILTIN ARGINFO    ArgInfo  #-}
-{-# BUILTIN ARGARGINFO arg-info #-}
-{-# BUILTIN ARG        Arg      #-}
-{-# BUILTIN ARGARG     arg      #-}
-
-data Blocker : Set where
-  blockerAny  : List Blocker → Blocker
-  blockerAll  : List Blocker → Blocker
-  blockerMeta : Meta → Blocker
-
-{-# BUILTIN AGDABLOCKER     Blocker #-}
-{-# BUILTIN AGDABLOCKERANY  blockerAny #-}
-{-# BUILTIN AGDABLOCKERALL  blockerAll #-}
-{-# BUILTIN AGDABLOCKERMETA blockerMeta #-}
-
--- Name abstraction --
-
-data Abs {a} (A : Set a) : Set a where
-  abs : (s : String) (x : A) → Abs A
-
-{-# BUILTIN ABS    Abs #-}
-{-# BUILTIN ABSABS abs #-}
-
--- Literals --
-
-data Literal : Set where
-  nat    : (n : Nat)    → Literal
-  word64 : (n : Word64) → Literal
-  float  : (x : Float)  → Literal
-  char   : (c : Char)   → Literal
-  string : (s : String) → Literal
-  name   : (x : Name)   → Literal
-  meta   : (x : Meta)   → Literal
-
-{-# BUILTIN AGDALITERAL   Literal #-}
-{-# BUILTIN AGDALITNAT    nat     #-}
-{-# BUILTIN AGDALITWORD64 word64  #-}
-{-# BUILTIN AGDALITFLOAT  float   #-}
-{-# BUILTIN AGDALITCHAR   char    #-}
-{-# BUILTIN AGDALITSTRING string  #-}
-{-# BUILTIN AGDALITQNAME  name    #-}
-{-# BUILTIN AGDALITMETA   meta    #-}
-
-
--- Terms and patterns --
-
-data Term    : Set
-data Sort    : Set
-data Pattern : Set
-data Clause  : Set
-Type = Term
-Telescope = List (Σ String λ _ → Arg Type)
-
-data Term where
-  var       : (x : Nat) (args : List (Arg Term)) → Term
-  con       : (c : Name) (args : List (Arg Term)) → Term
-  def       : (f : Name) (args : List (Arg Term)) → Term
-  lam       : (v : Visibility) (t : Abs Term) → Term
-  pat-lam   : (cs : List Clause) (args : List (Arg Term)) → Term
-  pi        : (a : Arg Type) (b : Abs Type) → Term
-  agda-sort : (s : Sort) → Term
-  lit       : (l : Literal) → Term
-  meta      : (x : Meta) → List (Arg Term) → Term
-  unknown   : Term
-
-data Sort where
-  set     : (t : Term) → Sort
-  lit     : (n : Nat) → Sort
-  prop    : (t : Term) → Sort
-  propLit : (n : Nat) → Sort
-  inf     : (n : Nat) → Sort
-  unknown : Sort
-
-data Pattern where
-  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
-  dot    : (t : Term)    → Pattern
-  var    : (x : Nat)     → Pattern
-  lit    : (l : Literal) → Pattern
-  proj   : (f : Name)    → Pattern
-  absurd : (x : Nat)     → Pattern  -- absurd patterns counts as variables
-
-data Clause where
-  clause        : (tel : Telescope) (ps : List (Arg Pattern)) (t : Term) → Clause
-  absurd-clause : (tel : Telescope) (ps : List (Arg Pattern)) → Clause
-
-{-# BUILTIN AGDATERM      Term    #-}
-{-# BUILTIN AGDASORT      Sort    #-}
-{-# BUILTIN AGDAPATTERN   Pattern #-}
-{-# BUILTIN AGDACLAUSE    Clause  #-}
-
-{-# BUILTIN AGDATERMVAR         var       #-}
-{-# BUILTIN AGDATERMCON         con       #-}
-{-# BUILTIN AGDATERMDEF         def       #-}
-{-# BUILTIN AGDATERMMETA        meta      #-}
-{-# BUILTIN AGDATERMLAM         lam       #-}
-{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
-{-# BUILTIN AGDATERMPI          pi        #-}
-{-# BUILTIN AGDATERMSORT        agda-sort #-}
-{-# BUILTIN AGDATERMLIT         lit       #-}
-{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}
-
-{-# BUILTIN AGDASORTSET         set     #-}
-{-# BUILTIN AGDASORTLIT         lit     #-}
-{-# BUILTIN AGDASORTPROP        prop    #-}
-{-# BUILTIN AGDASORTPROPLIT     propLit #-}
-{-# BUILTIN AGDASORTINF         inf     #-}
-{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
-
-{-# BUILTIN AGDAPATCON    con     #-}
-{-# BUILTIN AGDAPATDOT    dot     #-}
-{-# BUILTIN AGDAPATVAR    var     #-}
-{-# BUILTIN AGDAPATLIT    lit     #-}
-{-# BUILTIN AGDAPATPROJ   proj    #-}
-{-# BUILTIN AGDAPATABSURD absurd  #-}
-
-{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
-{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
-
--- Definitions --
-
-data Definition : Set where
-  function    : (cs : List Clause) → Definition
-  data-type   : (pars : Nat) (cs : List Name) → Definition
-  record-type : (c : Name) (fs : List (Arg Name)) → Definition
-  data-cons   : (d : Name) → Definition
-  axiom       : Definition
-  prim-fun    : Definition
-
-{-# BUILTIN AGDADEFINITION                Definition  #-}
-{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
-{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
-{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
-{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
-{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
-{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}
-
--- Errors --
-
-data ErrorPart : Set where
-  strErr  : String → ErrorPart
-  termErr : Term → ErrorPart
-  pattErr : Pattern → ErrorPart
-  nameErr : Name → ErrorPart
-
-{-# BUILTIN AGDAERRORPART       ErrorPart #-}
-{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
-{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
-{-# BUILTIN AGDAERRORPARTPATT   pattErr   #-}
-{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}
-
--- TC monad --
-
-postulate
-  TC               : ∀ {a} → Set a → Set a
-  returnTC         : ∀ {a} {A : Set a} → A → TC A
-  bindTC           : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
-  unify            : Term → Term → TC ⊤
-  typeError        : ∀ {a} {A : Set a} → List ErrorPart → TC A
-  inferType        : Term → TC Type
-  checkType        : Term → Type → TC Term
-  normalise        : Term → TC Term
-  reduce           : Term → TC Term
-  catchTC          : ∀ {a} {A : Set a} → TC A → TC A → TC A
-  quoteTC          : ∀ {a} {A : Set a} → A → TC Term
-  unquoteTC        : ∀ {a} {A : Set a} → Term → TC A
-  quoteωTC         : ∀ {A : Setω} → A → TC Term
-  getContext       : TC Telescope
-  extendContext    : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A
-  inContext        : ∀ {a} {A : Set a} → Telescope → TC A → TC A
-  freshName        : String → TC Name
-  declareDef       : Arg Name → Type → TC ⊤
-  declarePostulate : Arg Name → Type → TC ⊤
-  declareData      : Name → Nat → Type → TC ⊤
-  defineData       : Name → List (Σ Name (λ _ → Type)) → TC ⊤
-  defineFun        : Name → List Clause → TC ⊤
-  getType          : Name → TC Type
-  getDefinition    : Name → TC Definition
-  blockTC          : ∀ {a} {A : Set a} → Blocker → TC A
-  commitTC         : TC ⊤
-  isMacro          : Name → TC Bool
-  pragmaForeign    : String → String → TC ⊤
-  pragmaCompile    : String → Name → String → TC ⊤
-
-  -- If 'true', makes the following primitives also normalise
-  -- their results: inferType, checkType, quoteTC, getType, and getContext
-  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
-  askNormalisation  : TC Bool
-
-  -- If 'true', makes the following primitives to reconstruct hidden arguments:
-  -- getDefinition, normalise, reduce, inferType, checkType and getContext
-  withReconstructed : ∀ {a} {A : Set a} → Bool → TC A → TC A
-  askReconstructed  : TC Bool
-
-  -- Whether implicit arguments at the end should be turned into metavariables
-  withExpandLast : ∀ {a} {A : Set a} → Bool → TC A → TC A
-  askExpandLast  : TC Bool
-
-  -- White/blacklist specific definitions for reduction while executing the TC computation
-  -- 'true' for whitelist, 'false' for blacklist
-  withReduceDefs : ∀ {a} {A : Set a} → (Σ Bool λ _ → List Name) → TC A → TC A
-  askReduceDefs  : TC (Σ Bool λ _ → List Name)
-
-  formatErrorParts : List ErrorPart → TC String
-  -- Prints the third argument if the corresponding verbosity level is turned
-  -- on (with the -v flag to Agda).
-  debugPrint : String → Nat → List ErrorPart → TC ⊤
-
-  -- Fail if the given computation gives rise to new, unsolved
-  -- "blocking" constraints.
-  noConstraints : ∀ {a} {A : Set a} → TC A → TC A
-
-  -- Run the given TC action and return the first component. Resets to
-  -- the old TC state if the second component is 'false', or keep the
-  -- new TC state if it is 'true'.
-  runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
-
-  -- Get a list of all possible instance candidates for the given meta
-  -- variable (it does not have to be an instance meta).
-  getInstances : Meta → TC (List Term)
-
-{-# BUILTIN AGDATCM                           TC                         #-}
-{-# BUILTIN AGDATCMRETURN                     returnTC                   #-}
-{-# BUILTIN AGDATCMBIND                       bindTC                     #-}
-{-# BUILTIN AGDATCMUNIFY                      unify                      #-}
-{-# BUILTIN AGDATCMTYPEERROR                  typeError                  #-}
-{-# BUILTIN AGDATCMINFERTYPE                  inferType                  #-}
-{-# BUILTIN AGDATCMCHECKTYPE                  checkType                  #-}
-{-# BUILTIN AGDATCMNORMALISE                  normalise                  #-}
-{-# BUILTIN AGDATCMREDUCE                     reduce                     #-}
-{-# BUILTIN AGDATCMCATCHERROR                 catchTC                    #-}
-{-# BUILTIN AGDATCMQUOTETERM                  quoteTC                    #-}
-{-# BUILTIN AGDATCMUNQUOTETERM                unquoteTC                  #-}
-{-# BUILTIN AGDATCMQUOTEOMEGATERM             quoteωTC                   #-}
-{-# BUILTIN AGDATCMGETCONTEXT                 getContext                 #-}
-{-# BUILTIN AGDATCMEXTENDCONTEXT              extendContext              #-}
-{-# BUILTIN AGDATCMINCONTEXT                  inContext                  #-}
-{-# BUILTIN AGDATCMFRESHNAME                  freshName                  #-}
-{-# BUILTIN AGDATCMDECLAREDEF                 declareDef                 #-}
-{-# BUILTIN AGDATCMDECLAREPOSTULATE           declarePostulate           #-}
-{-# BUILTIN AGDATCMDECLAREDATA                declareData                #-}
-{-# BUILTIN AGDATCMDEFINEDATA                 defineData                 #-}
-{-# BUILTIN AGDATCMDEFINEFUN                  defineFun                  #-}
-{-# BUILTIN AGDATCMGETTYPE                    getType                    #-}
-{-# BUILTIN AGDATCMGETDEFINITION              getDefinition              #-}
-{-# BUILTIN AGDATCMBLOCK                      blockTC                    #-}
-{-# BUILTIN AGDATCMCOMMIT                     commitTC                   #-}
-{-# BUILTIN AGDATCMISMACRO                    isMacro                    #-}
-{-# BUILTIN AGDATCMPRAGMAFOREIGN              pragmaForeign              #-}
-{-# BUILTIN AGDATCMPRAGMACOMPILE              pragmaCompile              #-}
-{-# BUILTIN AGDATCMWITHNORMALISATION          withNormalisation          #-}
-{-# BUILTIN AGDATCMWITHRECONSTRUCTED          withReconstructed          #-}
-{-# BUILTIN AGDATCMWITHEXPANDLAST             withExpandLast             #-}
-{-# BUILTIN AGDATCMWITHREDUCEDEFS             withReduceDefs             #-}
-{-# BUILTIN AGDATCMASKNORMALISATION           askNormalisation           #-}
-{-# BUILTIN AGDATCMASKRECONSTRUCTED           askReconstructed           #-}
-{-# BUILTIN AGDATCMASKEXPANDLAST              askExpandLast              #-}
-{-# BUILTIN AGDATCMASKREDUCEDEFS              askReduceDefs              #-}
-{-# BUILTIN AGDATCMFORMATERRORPARTS           formatErrorParts           #-}
-{-# BUILTIN AGDATCMDEBUGPRINT                 debugPrint                 #-}
-{-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
-{-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
-{-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}
-
--- All the TC primitives are compiled to functions that return
--- undefined, rather than just undefined, in an attempt to make sure
--- that code will run properly.
-{-# COMPILE JS returnTC          = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS bindTC            = _ => _ => _ => _ =>
-                                   _ => _ =>           undefined #-}
-{-# COMPILE JS unify             = _ => _ =>           undefined #-}
-{-# COMPILE JS typeError         = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS inferType         = _ =>                undefined #-}
-{-# COMPILE JS checkType         = _ => _ =>           undefined #-}
-{-# COMPILE JS normalise         = _ =>                undefined #-}
-{-# COMPILE JS reduce            = _ =>                undefined #-}
-{-# COMPILE JS catchTC           = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS quoteTC           = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS unquoteTC         = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS quoteωTC          = _ => _ =>           undefined #-}
-{-# COMPILE JS getContext        =                     undefined #-}
-{-# COMPILE JS extendContext     = _ => _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS inContext         = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS freshName         = _ =>                undefined #-}
-{-# COMPILE JS declareDef        = _ => _ =>           undefined #-}
-{-# COMPILE JS declarePostulate  = _ => _ =>           undefined #-}
-{-# COMPILE JS declareData       = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS defineData        = _ => _ =>           undefined #-}
-{-# COMPILE JS defineFun         = _ => _ =>           undefined #-}
-{-# COMPILE JS getType           = _ =>                undefined #-}
-{-# COMPILE JS getDefinition     = _ =>                undefined #-}
-{-# COMPILE JS blockTC           = _ => _ =>           undefined #-}
-{-# COMPILE JS commitTC          =                     undefined #-}
-{-# COMPILE JS isMacro           = _ =>                undefined #-}
-{-# COMPILE JS pragmaForeign     = _ => _ =>           undefined #-}
-{-# COMPILE JS pragmaCompile     = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS withNormalisation = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS withReconstructed = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS withExpandLast    = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS withReduceDefs    = _ => _ => _ => _ => undefined #-}
-{-# COMPILE JS askNormalisation  =                     undefined #-}
-{-# COMPILE JS askReconstructed  =                     undefined #-}
-{-# COMPILE JS askExpandLast     =                     undefined #-}
-{-# COMPILE JS askReduceDefs     =                     undefined #-}
-{-# COMPILE JS debugPrint        = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS noConstraints     = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS runSpeculative    = _ => _ => _ =>      undefined #-}
-{-# COMPILE JS getInstances      = _ =>                undefined #-}
-
-private
-  filter : (Name → Bool) → List Name → List Name
-  filter p [] = []
-  filter p (x ∷ xs) with p x
-  ... | true  = x ∷ filter p xs
-  ... | false = filter p xs
-
-  _∈_ : Name → List Name → Bool
-  n ∈ []      = false
-  n ∈ (n' ∷ l) with primQNameEquality n n'
-  ... | true  = true
-  ... | false = n ∈ l
-
-  _∉_ : Name → List Name → Bool
-  n ∉ l with n ∈ l
-  ... | true  = false
-  ... | false = true
-
-  _++_ : List Name → List Name → List Name
-  [] ++ l       = l
-  (x ∷ xs) ++ l = x ∷ (xs ++ l)
-
-  combineReduceDefs : (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name)
-  combineReduceDefs (true  , defs₁) (true  , defs₂) = (true  , filter (_∈ defs₁) defs₂)
-  combineReduceDefs (false , defs₁) (true  , defs₂) = (true  , filter (_∉ defs₁) defs₂)
-  combineReduceDefs (true  , defs₁) (false , defs₂) = (true  , filter (_∉ defs₂) defs₁)
-  combineReduceDefs (false , defs₁) (false , defs₂) = (false , defs₁ ++ defs₂)
-
-onlyReduceDefs dontReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A
-onlyReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (true  , defs) exDefs) x)
-dontReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (false , defs) exDefs) x)
-
-blockOnMeta   : ∀ {a} {A : Set a} → Meta → TC A
-blockOnMeta m = blockTC (blockerMeta m)
-
-{-# WARNING_ON_USAGE onlyReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `onlyReduceDefs`" #-}
-{-# WARNING_ON_USAGE dontReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `dontReduceDefs`" #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Sigma.html b/lib/Agda.Builtin.Sigma.html deleted file mode 100644 index 1aa3a993..00000000 --- a/lib/Agda.Builtin.Sigma.html +++ /dev/null @@ -1,19 +0,0 @@ - -Agda.Builtin.Sigma
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Sigma where
-
-open import Agda.Primitive
-
-record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
-  constructor _,_
-  field
-    fst : A
-    snd : B fst
-
-open Σ public
-
-infixr 4 _,_
-
-{-# BUILTIN SIGMA Σ #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Strict.html b/lib/Agda.Builtin.Strict.html deleted file mode 100644 index 7b38c5c8..00000000 --- a/lib/Agda.Builtin.Strict.html +++ /dev/null @@ -1,11 +0,0 @@ - -Agda.Builtin.Strict
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Strict where
-
-open import Agda.Builtin.Equality
-
-primitive
-  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
-  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.String.html b/lib/Agda.Builtin.String.html deleted file mode 100644 index 217bfdd4..00000000 --- a/lib/Agda.Builtin.String.html +++ /dev/null @@ -1,38 +0,0 @@ - -Agda.Builtin.String
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.String where
-
-open import Agda.Builtin.Bool
-open import Agda.Builtin.Char
-open import Agda.Builtin.List
-open import Agda.Builtin.Maybe
-open import Agda.Builtin.Nat using (Nat)
-open import Agda.Builtin.Sigma
-
-postulate String : Set
-{-# BUILTIN STRING String #-}
-
-primitive
-  primStringUncons   : String → Maybe (Σ Char (λ _ → String))
-  primStringToList   : String → List Char
-  primStringFromList : List Char → String
-  primStringAppend   : String → String → String
-  primStringEquality : String → String → Bool
-  primShowChar       : Char → String
-  primShowString     : String → String
-  primShowNat        : Nat → String
-
-{-# COMPILE JS primStringUncons = function(x) {
-   if (x === "") { return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"]; };
-   return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](z_jAgda_Agda_Builtin_Sigma["_,_"](x.charAt(0))(x.slice(1)));
-   }
- #-}
-{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}
-{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-}
-{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-}
-{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-}
-{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-}
-{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-}
-{-# COMPILE JS primShowNat = function(x) { return JSON.stringify(x); } #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Unit.html b/lib/Agda.Builtin.Unit.html deleted file mode 100644 index ef3fcda6..00000000 --- a/lib/Agda.Builtin.Unit.html +++ /dev/null @@ -1,12 +0,0 @@ - -Agda.Builtin.Unit
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Unit where
-
-record ⊤ : Set where
-  instance constructor tt
-
-{-# BUILTIN UNIT ⊤ #-}
-{-# COMPILE GHC ⊤ = data () (()) #-}
-
\ No newline at end of file diff --git a/lib/Agda.Builtin.Word.html b/lib/Agda.Builtin.Word.html deleted file mode 100644 index 5267ee5b..00000000 --- a/lib/Agda.Builtin.Word.html +++ /dev/null @@ -1,15 +0,0 @@ - -Agda.Builtin.Word
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --level-universe #-}
-
-module Agda.Builtin.Word where
-
-open import Agda.Builtin.Nat
-
-postulate Word64 : Set
-{-# BUILTIN WORD64 Word64 #-}
-
-primitive
-  primWord64ToNat   : Word64 → Nat
-  primWord64FromNat : Nat → Word64
-
\ No newline at end of file diff --git a/lib/Agda.Primitive.html b/lib/Agda.Primitive.html deleted file mode 100644 index 3f6bab08..00000000 --- a/lib/Agda.Primitive.html +++ /dev/null @@ -1,43 +0,0 @@ - -Agda.Primitive
-- The Agda primitives (preloaded).
-
-{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
-
-module Agda.Primitive where
-
-------------------------------------------------------------------------
--- Universe levels
-------------------------------------------------------------------------
-
-infixl 6 _⊔_
-
-{-# BUILTIN PROP           Prop      #-}
-{-# BUILTIN TYPE           Set       #-}
-{-# BUILTIN STRICTSET      SSet      #-}
-
-{-# BUILTIN PROPOMEGA      Propω     #-}
-{-# BUILTIN SETOMEGA       Setω      #-}
-{-# BUILTIN STRICTSETOMEGA SSetω     #-}
-
-{-# BUILTIN LEVELUNIV      LevelUniv #-}
-
--- Level is the first thing we need to define.
--- The other postulates can only be checked if built-in Level is known.
-
-postulate
-  Level : LevelUniv
-
--- MAlonzo compiles Level to (). This should be safe, because it is
--- not possible to pattern match on levels.
-
-{-# BUILTIN LEVEL Level #-}
-
-postulate
-  lzero : Level
-  lsuc  : (ℓ : Level) → Level
-  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level
-
-{-# BUILTIN LEVELZERO lzero #-}
-{-# BUILTIN LEVELSUC  lsuc  #-}
-{-# BUILTIN LEVELMAX  _⊔_   #-}
-
\ No newline at end of file diff --git a/lib/Agda.css b/lib/Agda.css deleted file mode 100644 index 86813a50..00000000 --- a/lib/Agda.css +++ /dev/null @@ -1,41 +0,0 @@ -/* Aspects. */ -.Agda .Comment { color: #B22222 } -.Agda .Background {} -.Agda .Markup { color: #000000 } -.Agda .Keyword { color: #CD6600 } -.Agda .String { color: #B22222 } -.Agda .Number { color: #A020F0 } -.Agda .Symbol { color: #404040 } -.Agda .PrimitiveType { color: #0000CD } -.Agda .Pragma { color: black } -.Agda .Operator {} -.Agda .Hole { background: #B4EEB4 } - -/* NameKinds. */ -.Agda .Bound { color: black } -.Agda .Generalizable { color: black } -.Agda .InductiveConstructor { color: #008B00 } -.Agda .CoinductiveConstructor { color: #8B7500 } -.Agda .Datatype { color: #0000CD } -.Agda .Field { color: #EE1289 } -.Agda .Function { color: #0000CD } -.Agda .Module { color: #A020F0 } -.Agda .Postulate { color: #0000CD } -.Agda .Primitive { color: #0000CD } -.Agda .Record { color: #0000CD } - -/* OtherAspects. */ -.Agda .DottedPattern {} -.Agda .UnsolvedMeta { color: black; background: yellow } -.Agda .UnsolvedConstraint { color: black; background: yellow } -.Agda .TerminationProblem { color: black; background: #FFA07A } -.Agda .IncompletePattern { color: black; background: #F5DEB3 } -.Agda .Error { color: red; text-decoration: underline } -.Agda .TypeChecks { color: black; background: #ADD8E6 } -.Agda .Deadcode { color: black; background: #808080 } -.Agda .ShadowingInTelescope { color: black; background: #808080 } - -/* Standard attributes. */ -.Agda a { text-decoration: none } -.Agda a[href]:hover { background-color: #B4EEB4 } -.Agda [href].hover-highlight { background-color: #B4EEB4; } diff --git a/lib/Haskell.Prelude.html b/lib/Haskell.Prelude.html deleted file mode 100644 index d2f1e269..00000000 --- a/lib/Haskell.Prelude.html +++ /dev/null @@ -1,144 +0,0 @@ - -Haskell.Prelude
{-# OPTIONS --no-auto-inline #-}
-module Haskell.Prelude where
-
-open import Haskell.Prim
-open Haskell.Prim public using
-  ( Bool; True; False; Char; Integer;
-    List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
-    IsTrue; IsFalse; NonEmpty;
-    All; allNil; allCons;
-    Any; anyHere; anyThere;
-    id; _∘_; _$_; flip; const;
-    if_then_else_; case_of_;
-    Number; fromNat; Negative; fromNeg;
-    IsString; fromString;
-    _≡_; refl;
-    a; b; c; d; e; f; m; s; t )
-
-open import Haskell.Prim.Absurd      public
-open import Haskell.Prim.Applicative public
-open import Haskell.Prim.Bool        public
-open import Haskell.Prim.Bounded     public
-open import Haskell.Prim.Char        public
-open import Haskell.Prim.Double      public
-open import Haskell.Prim.Either      public
-open import Haskell.Prim.Enum        public
-open import Haskell.Prim.Eq          public
-open import Haskell.Prim.Foldable    public
-open import Haskell.Prim.Functor     public
-open import Haskell.Prim.Int         public
-open import Haskell.Prim.Integer     public
-open import Haskell.Prim.IO          public
-open import Haskell.Prim.List        public
-open import Haskell.Prim.Maybe       public
-open import Haskell.Prim.Monad       public
-open import Haskell.Prim.Monoid      public
-open import Haskell.Prim.Num         public
-open import Haskell.Prim.Ord         public
-open import Haskell.Prim.Show        public
-open import Haskell.Prim.String      public
-open import Haskell.Prim.Traversable public
-open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
-open import Haskell.Prim.Word        public
-
--- Problematic features
---  - [Partial]:  Could pass implicit/instance arguments to prove totality.
---  - [Float]:    Or Float (Agda floats are Doubles)
---  - [Infinite]: Define colists and map to Haskell lists?
-
--- Missing from the Haskell Prelude:
---
---     Float        [Float]
---     Rational
---
---     Real(toRational),
---     Integral(quot, rem, div, mod, quotRem, divMod, toInteger),
---     Fractional((/), recip, fromRational),
---     Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,
---              asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),
---     RealFrac(properFraction, truncate, round, ceiling, floor),
---     RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
---               encodeFloat, exponent, significand, scaleFloat, isNaN,
---               isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
---
---     subtract, even, odd, gcd, lcm, (^), (^^),
---     fromIntegral, realToFrac,
---
---     foldr1, foldl1, maximum, minimum      [Partial]
---
---     until [Partial]
---
---     iterate, repeat, cycle          [Infinite]
---
---     ReadS, Read(readsPrec, readList),
---     reads, readParen, read, lex,
---
---     IO, putChar, putStr, putStrLn, print,
---     getChar, getLine, getContents, interact,
---     FilePath, readFile, writeFile, appendFile, readIO, readLn,
---     IOError, ioError, userError,
-
-
---------------------------------------------------
--- Functions
-
-infixr 0 _$!_
-
-_$!_ : (a → b) → a → b
-_$!_ = _$_
-
-seq : a → b → b
-seq = const id
-
-asTypeOf : a → a → a
-asTypeOf x _ = x
-
-undefined : {@0 @(tactic absurd) i : ⊥} → a
-undefined {i = ()}
-
-error : {@0 @(tactic absurd) i : ⊥} → String → a
-error {i = ()} err
-
-errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
-errorWithoutStackTrace {i = ()} err
-
--------------------------------------------------
--- More List functions
---   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
---   turning those dependencies around.
-
-reverse : List a → List a
-reverse = foldl (flip _∷_) []
-
-infixl 9 _!!_ _!!ᴺ_
-
-_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
-(x ∷ xs) !!ᴺ zero  = x
-(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n
-
-_!!_ : (xs : List a) (n : Int)
-     → ⦃ @0 nn : IsNonNegativeInt n ⦄
-     → ⦃ @0 _  : IsTrue (intToNat n {{nn}} < lengthNat xs) ⦄ → a
-xs !! n = xs !!ᴺ intToNat n
-
-lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
-lookup x []              = Nothing
-lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
-
-
--------------------------------------------------
--- Unsafe functions
-
-coerce : @0 a ≡ b → a → b
-coerce refl x = x
-
-IsJust : Maybe a → Set
-IsJust Nothing  = ⊥
-IsJust (Just _) = ⊤
-
-fromJust : (x : Maybe a) → @0 {IsJust x} → a
-fromJust Nothing  = error "fromJust Nothing"
-fromJust (Just x) = x
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Absurd.html b/lib/Haskell.Prim.Absurd.html deleted file mode 100644 index 95feecde..00000000 --- a/lib/Haskell.Prim.Absurd.html +++ /dev/null @@ -1,25 +0,0 @@ - -Haskell.Prim.Absurd
-module Haskell.Prim.Absurd where
-
-open import Haskell.Prim
-
-open import Agda.Builtin.Reflection renaming (bindTC to _>>=_; absurd to absurdP)
-
-private
-
-  pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x
-
-  refute : Nat → Term
-  refute i = def (quote _$_) ( vArg (pat-lam (absurd-clause [] (vArg (absurdP 0) ∷ []) ∷ []) [])
-                             ∷ vArg (var i []) ∷ [])
-
-  tryRefute : Nat → Term → TC ⊤
-  tryRefute 0       _    = typeError (strErr "No variable of empty type found in the context" ∷ [])
-  tryRefute (suc n) hole = catchTC (unify hole (refute n)) (tryRefute n hole)
-
-absurd : Term → TC ⊤
-absurd hole = do
-  Γ ← getContext
-  tryRefute (lengthNat Γ) hole
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Applicative.html b/lib/Haskell.Prim.Applicative.html deleted file mode 100644 index 3d84fb89..00000000 --- a/lib/Haskell.Prim.Applicative.html +++ /dev/null @@ -1,85 +0,0 @@ - -Haskell.Prim.Applicative
module Haskell.Prim.Applicative where
-
-open import Haskell.Prim
-open import Haskell.Prim.Either
-open import Haskell.Prim.Foldable
-open import Haskell.Prim.Functor
-open import Haskell.Prim.IO
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Monoid
-open import Haskell.Prim.Tuple
-
-
---------------------------------------------------
--- Applicative
-
--- ** base
-record Applicative (f : Set → Set) : Set₁ where
-  infixl 4 _<*>_ _<*_ _*>_
-  field
-    pure  : a → f a
-    _<*>_ : f (a → b) → f a → f b
-    overlap ⦃ super ⦄ : Functor f
-    _<*_ : f a → f b → f a
-    _*>_ : f a → f b → f b
--- ** defaults
-record DefaultApplicative (f : Set → Set) : Set₁ where
-  constructor mk
-  infixl 4 _<*>_ _<*_ _*>_
-  field
-    pure  : a → f a
-    _<*>_ : f (a → b) → f a → f b
-    overlap ⦃ super ⦄ : Functor f
-
-  _<*_ : f a → f b → f a
-  x <* y = const <$> x <*> y
-
-  _*>_ : f a → f b → f b
-  x *> y = const id <$> x <*> y
--- ** export
-open Applicative ⦃...⦄ public
-{-# COMPILE AGDA2HS Applicative existing-class #-}
--- ** instances
-private
-  mkApplicative : DefaultApplicative t → Applicative t
-  mkApplicative x = record {DefaultApplicative x}
-instance
-  open DefaultApplicative
-
-  iApplicativeList : Applicative List
-  iApplicativeList = mkApplicative λ where
-    .pure x      → x ∷ []
-    ._<*>_ fs xs → concatMap (λ f → map f xs) fs
-
-  iApplicativeMaybe : Applicative Maybe
-  iApplicativeMaybe = mkApplicative λ where
-    .pure → Just
-    ._<*>_ (Just f) (Just x) → Just (f x)
-    ._<*>_ _        _        → Nothing
-
-  iApplicativeEither : Applicative (Either a)
-  iApplicativeEither = mkApplicative λ where
-    .pure → Right
-    ._<*>_ (Right f) (Right x) → Right (f x)
-    ._<*>_ (Left e)  _         → Left e
-    ._<*>_ _         (Left e)  → Left e
-
-  iApplicativeFun : Applicative (λ b → a → b)
-  iApplicativeFun = mkApplicative λ where
-    .pure        → const
-    ._<*>_ f g x → f x (g x)
-
-  iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
-  iApplicativeTuple₂ = mkApplicative λ where
-    .pure x                → mempty , x
-    ._<*>_ (a , f) (b , x) → a <> b , f x
-
-  iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
-  iApplicativeTuple₃ = mkApplicative λ where
-    .pure x                → mempty , mempty , x
-    ._<*>_ (a , u , f) (b , v , x) → a <> b , u <> v , f x
-
-instance postulate iApplicativeIO : Applicative IO
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Bool.html b/lib/Haskell.Prim.Bool.html deleted file mode 100644 index 36ec9c7c..00000000 --- a/lib/Haskell.Prim.Bool.html +++ /dev/null @@ -1,26 +0,0 @@ - -Haskell.Prim.Bool
-module Haskell.Prim.Bool where
-
-open import Haskell.Prim
-
---------------------------------------------------
--- Booleans
-
-infixr 3 _&&_
-_&&_ : Bool → Bool → Bool
-False && _ = False
-True  && x = x
-
-infixr 2 _||_
-_||_ : Bool → Bool → Bool
-False || x = x
-True  || _ = True
-
-not : Bool → Bool
-not False = True
-not True  = False
-
-otherwise : Bool
-otherwise = True
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Bounded.html b/lib/Haskell.Prim.Bounded.html deleted file mode 100644 index 13635e3f..00000000 --- a/lib/Haskell.Prim.Bounded.html +++ /dev/null @@ -1,96 +0,0 @@ - -Haskell.Prim.Bounded
-module Haskell.Prim.Bounded where
-
-open import Haskell.Prim
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Int
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Ord
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Word
-
---------------------------------------------------
--- Bounded
-
-record BoundedBelow (a : Set) : Set where
-  field
-    minBound : a
-
-record BoundedAbove (a : Set) : Set where
-  field
-    maxBound : a
-
-record Bounded (a : Set) : Set where
-  field
-    overlap ⦃ below ⦄ : BoundedBelow a
-    overlap ⦃ above ⦄ : BoundedAbove a
-
-{-# COMPILE AGDA2HS Bounded existing-class #-}
-
-open BoundedBelow ⦃...⦄ public
-open BoundedAbove ⦃...⦄ public
-
-instance
-  iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a
-  iBounded .Bounded.below = it
-  iBounded .Bounded.above = it
-
-instance
-  iBoundedBelowNat : BoundedBelow Nat
-  iBoundedBelowNat .minBound = 0
-
-  iBoundedBelowWord : BoundedBelow Word
-  iBoundedBelowWord .minBound = 0
-  iBoundedAboveWord : BoundedAbove Word
-  iBoundedAboveWord .maxBound = 18446744073709551615
-
-  iBoundedBelowInt : BoundedBelow Int
-  iBoundedBelowInt .minBound = -9223372036854775808
-  iBoundedAboveInt : BoundedAbove Int
-  iBoundedAboveInt .maxBound = 9223372036854775807
-
-  iBoundedBelowBool : BoundedBelow Bool
-  iBoundedBelowBool .minBound = False
-  iBoundedAboveBool : BoundedAbove Bool
-  iBoundedAboveBool .maxBound = True
-
-  iBoundedBelowChar : BoundedBelow Char
-  iBoundedBelowChar .minBound = '\0'
-  iBoundedAboveChar : BoundedAbove Char
-  iBoundedAboveChar .maxBound = '\1114111'
-
-  iBoundedBelowUnit : BoundedBelow ⊤
-  iBoundedBelowUnit .minBound = tt
-
-  iBoundedAboveUnit : BoundedAbove ⊤
-  iBoundedAboveUnit .maxBound = tt
-
-  iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄
-                      → BoundedBelow (a × b)
-  iBoundedBelowTuple₂ .minBound = minBound , minBound
-  iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄
-                      → BoundedAbove (a × b)
-  iBoundedAboveTuple₂ .maxBound = maxBound , maxBound
-
-  iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄
-                      → BoundedBelow (a × b × c)
-  iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound
-  iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄
-                      → BoundedAbove (a × b × c)
-  iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound
-
-  iBoundedBelowOrdering : BoundedBelow Ordering
-  iBoundedBelowOrdering .minBound = LT
-  iBoundedAboveOrdering : BoundedAbove Ordering
-  iBoundedAboveOrdering .maxBound = GT
-
--- Sanity checks
-
-private
-  _ : addWord maxBound 1 ≡ minBound
-  _ = refl
-
-  _ : addInt maxBound 1 ≡ minBound
-  _ = refl
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Char.html b/lib/Haskell.Prim.Char.html deleted file mode 100644 index 5cef9fd6..00000000 --- a/lib/Haskell.Prim.Char.html +++ /dev/null @@ -1,11 +0,0 @@ - -Haskell.Prim.Char
module Haskell.Prim.Char where
-
-open import Haskell.Prim
-
-import Agda.Builtin.Char 
-open Agda.Builtin.Char using (Char)
-    
-eqChar : Char → Char → Bool
-eqChar a b = eqNat (c2n a) (c2n b)
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Double.html b/lib/Haskell.Prim.Double.html deleted file mode 100644 index 62772ace..00000000 --- a/lib/Haskell.Prim.Double.html +++ /dev/null @@ -1,17 +0,0 @@ - -Haskell.Prim.Double
-module Haskell.Prim.Double where
-
-open import Agda.Builtin.Float public renaming (Float to Double)
-
-open import Haskell.Prim
-
-instance
-  iNumberDouble : Number Double
-  iNumberDouble .Number.Constraint _ = ⊤
-  iNumberDouble .fromNat n = primNatToFloat n
-
-  iNegativeDouble : Negative Double
-  iNegativeDouble .Negative.Constraint _ = ⊤
-  iNegativeDouble .fromNeg n = primFloatMinus 0.0 (fromNat n)
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Either.html b/lib/Haskell.Prim.Either.html deleted file mode 100644 index 84887f84..00000000 --- a/lib/Haskell.Prim.Either.html +++ /dev/null @@ -1,22 +0,0 @@ - -Haskell.Prim.Either
-module Haskell.Prim.Either where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-
---------------------------------------------------
--- Either
-
-data Either (a b : Set) : Set where
-  Left  : a → Either a b
-  Right : b → Either a b
-
-either : (a → c) → (b → c) → Either a b → c
-either f g (Left  x) = f x
-either f g (Right y) = g y
-
-testBool : (b : Bool) → Either (IsFalse b) (IsTrue b)
-testBool False = Left  itsFalse
-testBool True  = Right itsTrue
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Enum.html b/lib/Haskell.Prim.Enum.html deleted file mode 100644 index 5a00531e..00000000 --- a/lib/Haskell.Prim.Enum.html +++ /dev/null @@ -1,205 +0,0 @@ - -Haskell.Prim.Enum
-module Haskell.Prim.Enum where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Bounded
-open import Haskell.Prim.Either
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Functor
-open import Haskell.Prim.Int
-open import Haskell.Prim.Integer
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Num
-open import Haskell.Prim.Ord
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Word
-
-
---------------------------------------------------
--- Enum
---    Assumptions: unbounded enums have no constraints on their
---    operations and bounded enums should work on all values between
---    minBound and maxBound. Unbounded enums do not support enumFrom
---    and enumFromThen (since they return infinite lists).
-
-IfBoundedBelow : Maybe (BoundedBelow a) → (⦃ BoundedBelow a ⦄ → Set) → Set
-IfBoundedBelow Nothing  k = ⊤
-IfBoundedBelow (Just i) k = k ⦃ i ⦄
-
-IfBoundedAbove : Maybe (BoundedAbove a) → (⦃ BoundedAbove a ⦄ → Set) → Set
-IfBoundedAbove Nothing  k = ⊤
-IfBoundedAbove (Just i) k = k ⦃ i ⦄
-
-record Enum (a : Set) : Set₁ where
-  field
-    BoundedBelowEnum : Maybe (BoundedBelow a)
-    BoundedAboveEnum : Maybe (BoundedAbove a)
-    fromEnum         : a → Int
-
-  private
-    IsBoundedBelow : Set
-    IsBoundedBelow = maybe ⊥ (λ _ → ⊤) BoundedBelowEnum
-
-    IsBoundedAbove : Set
-    IsBoundedAbove = maybe ⊥ (λ _ → ⊤) BoundedAboveEnum
-
-    TrueIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
-    TrueIfLB C = IfBoundedBelow BoundedBelowEnum (IsTrue C)
-
-    TrueIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
-    TrueIfUB C = IfBoundedAbove BoundedAboveEnum (IsTrue C)
-
-    FalseIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
-    FalseIfLB C = IfBoundedBelow BoundedBelowEnum (IsFalse C)
-
-    FalseIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
-    FalseIfUB C = IfBoundedAbove BoundedAboveEnum (IsFalse C)
-
-    minInt : ⦃ BoundedBelow a ⦄ → Int
-    minInt ⦃ _ ⦄ = fromEnum minBound
-
-    maxInt : ⦃ BoundedAbove a ⦄ → Int
-    maxInt ⦃ _ ⦄ = fromEnum maxBound
-
-  field
-    toEnum : (n : Int) → @0 ⦃ TrueIfLB (minInt <= n) ⦄ → @0 ⦃ TrueIfUB (n <= maxInt) ⦄ → a
-    succ   : (x : a) → @0 ⦃ FalseIfUB (fromEnum x == maxInt) ⦄ → a
-    pred   : (x : a) → @0 ⦃ FalseIfLB (fromEnum x == minInt) ⦄ → a
-
-    enumFrom       : @0 ⦃ IsBoundedAbove ⦄ → a → List a
-    enumFromTo     : a → a → List a
-    -- In the Prelude Enum instances `enumFromThenTo x x y` gives the
-    -- infinite list of `x`s. The constraint is a little bit stronger than it needs to be,
-    -- since it rules out different x and x₁ that maps to the same Int, but this saves us
-    -- requiring an Eq instance for `a`, and it's not a terrible limitation to not be able to
-    -- write [0, 2^64 .. 2^66].
-    enumFromThenTo : (x x₁ : a) → @0 ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → a → List a
-    enumFromThen   : @0 ⦃ IsBoundedBelow ⦄ → @0 ⦃ IsBoundedAbove ⦄ → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → List a
-
-open Enum ⦃...⦄ public
-
-{-# COMPILE AGDA2HS Enum existing-class #-}
-
-private
-  divNat : Nat → Nat → Nat
-  divNat a 0       = 0
-  divNat a (suc b) = div-helper 0 b a b
-
-  diff : Integer → Integer → Maybe Nat
-  diff a b =
-    case a - b of λ where
-      (pos n)    → Just n
-      (negsuc _) → Nothing
-
-  unsafeIntegerToNat : Integer → Nat
-  unsafeIntegerToNat (pos n) = n
-  unsafeIntegerToNat (negsuc _) = 0
-
-  integerFromCount : Integer → Integer → Nat → List Integer
-  integerFromCount a step 0       = []
-  integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n
-
-  integerFromTo : Integer → Integer → List Integer
-  integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a)
-
-  integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer
-  integerFromThenTo a a₁ b =
-    case compare a a₁ of λ where
-      LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a)
-      EQ → [] -- impossible
-      GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b)
-
-instance
-  iEnumInteger : Enum Integer
-  iEnumInteger .BoundedBelowEnum  = Nothing
-  iEnumInteger .BoundedAboveEnum  = Nothing
-  iEnumInteger .fromEnum          = integerToInt
-  iEnumInteger .toEnum          n = intToInteger n
-  iEnumInteger .succ              = _+ 1
-  iEnumInteger .pred              = _- 1
-  iEnumInteger .enumFromTo        = integerFromTo
-  iEnumInteger .enumFromThenTo    = integerFromThenTo
-
-module _ (from : a → Integer) (to : Integer → a) where
-  private
-    fromTo : a → a → List a
-    fromTo a b = map to (enumFromTo (from a) (from b))
-
-    fromThenTo : (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
-    fromThenTo a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
-
-  unboundedEnumViaInteger : Enum a
-  unboundedEnumViaInteger .BoundedBelowEnum      = Nothing
-  unboundedEnumViaInteger .BoundedAboveEnum      = Nothing
-  unboundedEnumViaInteger .fromEnum              = integerToInt ∘ from
-  unboundedEnumViaInteger .toEnum         n      = to (intToInteger n)
-  unboundedEnumViaInteger .succ           x      = to (from x + 1)
-  unboundedEnumViaInteger .pred           x      = to (from x - 1)
-  unboundedEnumViaInteger .enumFromTo     a b    = fromTo a b
-  unboundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedBelowEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedBelow a ⦄ → Enum a
-  boundedBelowEnumViaInteger .BoundedBelowEnum      = Just it
-  boundedBelowEnumViaInteger .BoundedAboveEnum      = Nothing
-  boundedBelowEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedBelowEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedBelowEnumViaInteger .succ           x      = to (from x + 1)
-  boundedBelowEnumViaInteger .pred           x      = to (from x - 1)
-  boundedBelowEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedBelowEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedAboveEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedAbove a ⦄ → Enum a
-  boundedAboveEnumViaInteger .BoundedBelowEnum      = Nothing
-  boundedAboveEnumViaInteger .BoundedAboveEnum      = Just it
-  boundedAboveEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedAboveEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedAboveEnumViaInteger .succ           x      = to (from x + 1)
-  boundedAboveEnumViaInteger .pred           x      = to (from x - 1)
-  boundedAboveEnumViaInteger .enumFrom       a      = fromTo a maxBound
-  boundedAboveEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedAboveEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-
-  boundedEnumViaInteger : ⦃ Ord a ⦄ → ⦃ Bounded a ⦄ → Enum a
-  boundedEnumViaInteger .BoundedBelowEnum      = Just it
-  boundedEnumViaInteger .BoundedAboveEnum      = Just it
-  boundedEnumViaInteger .fromEnum              = integerToInt ∘ from
-  boundedEnumViaInteger .toEnum         n      = to (intToInteger n)
-  boundedEnumViaInteger .succ           x      = to (from x + 1)
-  boundedEnumViaInteger .pred           x      = to (from x - 1)
-  boundedEnumViaInteger .enumFromTo     a b    = fromTo a b
-  boundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
-  boundedEnumViaInteger .enumFrom       a      = fromTo a maxBound
-  boundedEnumViaInteger .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo a a₁ maxBound
-              else fromThenTo a a₁ minBound
-
-instance
-  iEnumNat : Enum Nat
-  iEnumNat = boundedBelowEnumViaInteger pos unsafeIntegerToNat
-
-  iEnumInt : Enum Int
-  iEnumInt = boundedEnumViaInteger intToInteger integerToInt
-
-  iEnumWord : Enum Word
-  iEnumWord = boundedEnumViaInteger wordToInteger integerToWord
-
-  iEnumBool : Enum Bool
-  iEnumBool = boundedEnumViaInteger (if_then 1 else 0) (_/= 0)
-
-  iEnumOrdering : Enum Ordering
-  iEnumOrdering = boundedEnumViaInteger (λ where LT → 0; EQ → 1; GT → 2)
-                                        (λ where (pos 0) → LT; (pos 1) → EQ; _ → GT)
-
-  iEnumUnit : Enum ⊤
-  iEnumUnit = boundedEnumViaInteger (λ _ → 0) λ _ → tt
-
-  iEnumChar : Enum Char
-  iEnumChar = boundedEnumViaInteger (pos ∘ c2n)
-                                    λ where (pos n) → primNatToChar n; _ → '_'
-
-  -- Missing:
-  --  Enum Double  (can't go via Integer)
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Eq.html b/lib/Haskell.Prim.Eq.html deleted file mode 100644 index 4af39dea..00000000 --- a/lib/Haskell.Prim.Eq.html +++ /dev/null @@ -1,84 +0,0 @@ - -Haskell.Prim.Eq
-module Haskell.Prim.Eq where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Char
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Int
-open import Haskell.Prim.Word
-open import Haskell.Prim.Double
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
-
---------------------------------------------------
--- Eq
-
-record Eq (a : Set) : Set where
-  infix 4 _==_
-  field
-    _==_ : a → a → Bool
-
-open Eq ⦃...⦄ public
-
-{-# COMPILE AGDA2HS Eq existing-class #-}
-
-_/=_ : {{Eq a}} → a → a → Bool
-x /= y = not (x == y)
-
-infix 4 _/=_
-
-instance
-  iEqNat : Eq Nat
-  iEqNat ._==_ = eqNat
-
-  iEqInteger : Eq Integer
-  iEqInteger ._==_ = eqInteger
-
-  iEqInt : Eq Int
-  iEqInt ._==_ = eqInt
-
-  iEqWord : Eq Word
-  iEqWord ._==_ = eqWord
-
-  iEqDouble : Eq Double
-  iEqDouble ._==_ = primFloatEquality
-
-  iEqBool : Eq Bool
-  iEqBool ._==_ False False = True
-  iEqBool ._==_ True  True  = True
-  iEqBool ._==_ _     _     = False
-
-  iEqChar : Eq Char
-  iEqChar ._==_ = eqChar
-
-  iEqUnit : Eq ⊤
-  iEqUnit ._==_ _ _ = True
-
-  iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
-  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
-
-  iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
-  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
-
-  iEqList : ⦃ Eq a ⦄ → Eq (List a)
-  iEqList {a} ._==_ = eqList
-    where
-      eqList : List a → List a → Bool
-      eqList [] [] = True
-      eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys
-      eqList _ _ = False
-
-
-  iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a)
-  iEqMaybe ._==_ Nothing  Nothing  = True
-  iEqMaybe ._==_ (Just x) (Just y) = x == y
-  iEqMaybe ._==_ _        _        = False
-
-  iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b)
-  iEqEither ._==_ (Left  x) (Left  y) = x == y
-  iEqEither ._==_ (Right x) (Right y) = x == y
-  iEqEither ._==_ _        _          = False
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Foldable.html b/lib/Haskell.Prim.Foldable.html deleted file mode 100644 index 0ac96fb5..00000000 --- a/lib/Haskell.Prim.Foldable.html +++ /dev/null @@ -1,118 +0,0 @@ - -Haskell.Prim.Foldable
-module Haskell.Prim.Foldable where
-
-open import Haskell.Prim
-open import Haskell.Prim.Num hiding (abs)
-open import Haskell.Prim.Eq
-open import Haskell.Prim.List
-open import Haskell.Prim.Int
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Monoid
-
---------------------------------------------------
--- Foldable
-
--- ** base
-record Foldable (t : Set → Set) : Set₁ where
-  field
-    foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
-    foldr : (a → b → b) → b → t a → b
-    foldl : (b → a → b) → b → t a → b
-    any : (a → Bool) → t a → Bool
-    all : (a → Bool) → t a → Bool
-    and : t Bool → Bool
-    null : t a → Bool
-    or : t Bool → Bool
-    concat : t (List a) → List a
-    concatMap : (a → List b) → t a → List b
-    elem : ⦃ Eq a ⦄ → a → t a → Bool
-    notElem : ⦃ Eq a ⦄ → a → t a → Bool
-    toList : t a → List a
-    sum : ⦃ iNum : Num a ⦄ → t a → a
-    product : ⦃ iNum : Num a ⦄ → t a → a
-    length : t a → Int
--- ** defaults
-record DefaultFoldable (t : Set → Set) : Set₁ where
-  module M = Foldable {t = t}
-  field foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
-
-  foldr : (a → b → b) → b → t a → b
-  foldr f z t = foldMap ⦃ MonoidEndo ⦄ f t z
-
-  foldl : (b → a → b) → b → t a → b
-  foldl f z t = foldMap ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z
-
-  any : (a → Bool) → t a → Bool
-  any = foldMap ⦃ MonoidDisj ⦄
-
-  all : (a → Bool) → t a → Bool
-  all = foldMap ⦃ MonoidConj ⦄
-
-  and : t Bool → Bool
-  and = all id
-
-  or : t Bool → Bool
-  or = any id
-
-  null : t a → Bool
-  null = all (const False)
-
-  concat : t (List a) → List a
-  concat = foldMap id
-
-  concatMap : (a → List b) → t a → List b
-  concatMap = foldMap
-
-  elem : ⦃ Eq a ⦄ → a → t a → Bool
-  elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_)
-
-  notElem : ⦃ Eq a ⦄ → a → t a → Bool
-  notElem x t = not (elem x t)
-
-  toList : t a → List a
-  toList = foldr _∷_ []
-
-  sum : ⦃ iNum : Num a ⦄ → t a → a
-  sum = foldMap ⦃ MonoidSum ⦄ id
-
-  product : ⦃ iNum : Num a ⦄ → t a → a
-  product = foldMap ⦃ MonoidProduct ⦄ id
-
-  length : t a → Int
-  length = foldMap ⦃ MonoidSum ⦄ (const 1)
--- ** export
-open Foldable ⦃...⦄ public
-{-# COMPILE AGDA2HS Foldable existing-class #-}
-
--- ** instances
-private
-  mkFoldable : DefaultFoldable t → Foldable t
-  mkFoldable x = record {DefaultFoldable x}
-
-  foldMap=_ : (∀ {b a} → ⦃ Monoid b ⦄ → (a → b) → t a → b) → Foldable t
-  foldMap= x = record {DefaultFoldable (record {foldMap = x})}
-instance
-  iFoldableList : Foldable List
-  iFoldableList = foldMap= foldMapList
-    where
-      foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
-      foldMapList f []       = mempty
-      foldMapList f (x ∷ xs) = f x <> foldMapList f xs
-
-  iFoldableMaybe : Foldable Maybe
-  iFoldableMaybe = foldMap= λ where
-    _ Nothing  → mempty
-    f (Just x) → f x
-
-  iFoldableEither : Foldable (Either a)
-  iFoldableEither = foldMap= λ where
-    _ (Left _)  → mempty
-    f (Right x) → f x
-
-  iFoldablePair : Foldable (a ×_)
-  iFoldablePair = foldMap= λ f (_ , x) → f x
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Functor.html b/lib/Haskell.Prim.Functor.html deleted file mode 100644 index e9b93875..00000000 --- a/lib/Haskell.Prim.Functor.html +++ /dev/null @@ -1,81 +0,0 @@ - -Haskell.Prim.Functor
-module Haskell.Prim.Functor where
-
-open import Haskell.Prim
-open import Haskell.Prim.Either
-open import Haskell.Prim.IO
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Tuple
-
---------------------------------------------------
--- Functor
-
--- ** base
-record Functor (f : Set → Set) : Set₁ where
-  infixl 1 _<&>_
-  infixl 4 _<$>_ _<$_ _$>_
-  field
-    fmap : (a → b) → f a → f b
-    _<$>_ : (a → b) → f a → f b
-    _<&>_ : f a → (a → b) → f b
-    _<$_ : (@0 {{ b }} → a) → f b → f a
-    _$>_ : f a → (@0 {{ a }} → b) → f b
-    void : f a → f ⊤
--- ** defaults
-record DefaultFunctor (f : Set → Set) : Set₁ where
-  field fmap : (a → b) → f a → f b
-
-  infixl 1 _<&>_
-  infixl 4 _<$>_ _<$_ _$>_
-
-  _<$>_ : (a → b) → f a → f b
-  _<$>_ = fmap
-
-  _<&>_ : f a → (a → b) → f b
-  m <&> f = fmap f m
-
-  _<$_ : (@0 {{ b }} → a) → f b → f a
-  x <$ m = fmap (λ b → x {{b}}) m
-
-  _$>_ : f a → (@0 {{ a }} → b) → f b
-  m $> x = x <$ m
-
-  void : f a → f ⊤
-  void = tt <$_
--- ** export
-open Functor ⦃...⦄ public
-{-# COMPILE AGDA2HS Functor existing-class #-}
--- ** instances
-private
-  mkFunctor : DefaultFunctor t → Functor t
-  mkFunctor x = record {DefaultFunctor x}
-
-  fmap=_ : (∀ {a b} → (a → b) → f a → f b) → Functor f
-  fmap= x = record {DefaultFunctor (record {fmap = x})}
-instance
-  iFunctorList : Functor List
-  iFunctorList = fmap= map
-
-  iFunctorMaybe : Functor Maybe
-  iFunctorMaybe = fmap= λ where
-    f Nothing  → Nothing
-    f (Just x) → Just (f x)
-
-  iFunctorEither : Functor (Either a)
-  iFunctorEither = fmap= λ where
-    f (Left  x) → Left x
-    f (Right y) → Right (f y)
-
-  iFunctorFun : Functor (λ b → a → b)
-  iFunctorFun = fmap= _∘_
-
-  iFunctorTuple₂ : Functor (a ×_)
-  iFunctorTuple₂ = fmap= λ f (x , y) → x , f y
-
-  iFunctorTuple₃ : Functor (a × b ×_)
-  iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z
-
-instance postulate iFunctiorIO : Functor IO
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.IO.html b/lib/Haskell.Prim.IO.html deleted file mode 100644 index 03f84638..00000000 --- a/lib/Haskell.Prim.IO.html +++ /dev/null @@ -1,29 +0,0 @@ - -Haskell.Prim.IO
module Haskell.Prim.IO where
-
-open import Haskell.Prim
-open import Haskell.Prim.Show
-open import Haskell.Prim.String
-
-postulate IO : ∀{a} → Set a → Set a
-
-FilePath = String
-
-postulate
-  -- Input functions
-  interact       : (String → String) → IO ⊤
-  getContents    : IO String
-  getLine        : IO String
-  getChar        : IO Char
-
-  -- Output functions
-  print          : ⦃ Show a ⦄ → a → IO ⊤
-  putChar        : Char → IO ⊤
-  putStr         : String → IO ⊤
-  putStrLn       : String → IO ⊤
-
-  -- Files
-  readFile       : FilePath → IO String
-  writeFile      : FilePath → String → IO ⊤
-  appendFile     : FilePath → String → IO ⊤
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Int.html b/lib/Haskell.Prim.Int.html deleted file mode 100644 index f4a08796..00000000 --- a/lib/Haskell.Prim.Int.html +++ /dev/null @@ -1,112 +0,0 @@ - -Haskell.Prim.Int
{-# OPTIONS --no-auto-inline #-}
-
--- Agda doesn't have an Int type (only Word64). With some work we
--- can represent signed ints using Word64.
-
-module Haskell.Prim.Int where
-
-open import Haskell.Prim
-open import Haskell.Prim.Word
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Bool
-
-
---------------------------------------------------
--- Definition
-
-data Int : Set where
-  int64 : Word64 → Int
-
-intToWord : Int → Word64
-intToWord (int64 a) = a
-
-unsafeIntToNat : Int → Nat
-unsafeIntToNat a = w2n (intToWord a)
-
-
---------------------------------------------------
--- Literals
-
-private
-  2⁶⁴ : Nat
-  2⁶⁴ = 18446744073709551616
-
-  2⁶³ : Nat
-  2⁶³ = 9223372036854775808
-
-  maxInt : Nat
-  maxInt = monusNat 2⁶³ 1
-
-instance
-  iNumberInt : Number Int
-  iNumberInt .Number.Constraint n = IsTrue (ltNat n 2⁶³)
-  iNumberInt .fromNat n = int64 (n2w n)
-
-  iNegativeInt : Negative Int
-  iNegativeInt .Negative.Constraint n = IsTrue (ltNat n (addNat 1 2⁶³))
-  iNegativeInt .fromNeg n = int64 (n2w (monusNat 2⁶⁴ n))
-
-
---------------------------------------------------
--- Arithmetic
-
-isNegativeInt : Int → Bool
-isNegativeInt (int64 w) = ltNat maxInt (w2n w)
-
-eqInt : Int → Int → Bool
-eqInt (int64 a) (int64 b) = eqNat (w2n a) (w2n b)
-
-negateInt : Int → Int
-negateInt (int64 a) = int64 (n2w (monusNat 2⁶⁴ (w2n a)))
-
-intToInteger : Int → Integer
-intToInteger a = if isNegativeInt a then negsuc (monusNat (unsafeIntToNat (negateInt a)) 1)
-                                    else pos (unsafeIntToNat a)
-
-integerToInt : Integer → Int
-integerToInt (pos    n) = int64 (n2w n)
-integerToInt (negsuc n) = negateInt (int64 (n2w (suc n)))
-
-private
-  ltPosInt : Int → Int → Bool
-  ltPosInt (int64 a) (int64 b) = ltWord a b
-
-ltInt : Int → Int → Bool
-ltInt a b with isNegativeInt a | isNegativeInt b
-... | True  | False = True
-... | False | True  = False
-... | True  | True  = ltPosInt (negateInt b) (negateInt a)
-... | False | False = ltPosInt a b
-
-addInt : Int → Int → Int
-addInt (int64 a) (int64 b) = int64 (addWord a b)
-
-subInt : Int → Int → Int
-subInt a b = addInt a (negateInt b)
-
-mulInt : Int → Int → Int
-mulInt (int64 a) (int64 b) = int64 (mulWord a b)
-
-absInt : Int → Int
-absInt a = if isNegativeInt a then negateInt a else a
-
-signInt : Int → Int
-signInt a = if      isNegativeInt a then -1
-            else if eqInt a 0       then 0 else 1
-
-showInt : Int → List Char
-showInt a = showInteger (intToInteger a)
-
-
---------------------------------------------------
--- Constraints
-
-IsNonNegativeInt : Int → Set
-IsNonNegativeInt a@(int64 _) =
-  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
-                     else ⊤
-
-intToNat : (a : Int) → @0 ⦃ IsNonNegativeInt a ⦄ → Nat
-intToNat a = unsafeIntToNat a
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Integer.html b/lib/Haskell.Prim.Integer.html deleted file mode 100644 index e5da7856..00000000 --- a/lib/Haskell.Prim.Integer.html +++ /dev/null @@ -1,108 +0,0 @@ - -Haskell.Prim.Integer
-module Haskell.Prim.Integer where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-
-{-|
-This module contains functions that should not be used
-within code that is supposed to be translated to Haskell.
-Nevertheless, these functions must be accessible for
-proofs (within the standard library).
-Hence, these functions are not flagged as private but
-instead are collected in a dedicated module that is not
-opened by default.
--}
-module Internal where
-  negNat : Nat → Integer
-  negNat 0       = pos 0
-  negNat (suc n) = negsuc n
-
-  subNat : Nat → Nat → Integer
-  subNat n       zero    = pos n
-  subNat zero    (suc m) = negsuc m
-  subNat (suc n) (suc m) = subNat n m
-open Internal
-
---------------------------------------------------
--- Literals
-
-
-instance
-  iNumberInteger : Number Integer
-  iNumberInteger .Number.Constraint _ = ⊤
-  iNumberInteger .fromNat n = pos n
-
-  iNegativeInteger : Negative Integer
-  iNegativeInteger .Negative.Constraint _ = ⊤
-  iNegativeInteger .fromNeg n = negNat n
-
-
---------------------------------------------------
--- Arithmetic
-
-negateInteger : Integer → Integer
-negateInteger (pos 0)       = pos 0
-negateInteger (pos (suc n)) = negsuc n
-negateInteger (negsuc n)    = pos (suc n)
-
-addInteger : Integer → Integer → Integer
-addInteger (pos    n) (pos    m) = pos (addNat n m)
-addInteger (pos    n) (negsuc m) = subNat n (suc m)
-addInteger (negsuc n) (pos    m) = subNat m (suc n)
-addInteger (negsuc n) (negsuc m) = negsuc (suc (addNat n m))
-
-subInteger : Integer → Integer → Integer
-subInteger n m = addInteger n (negateInteger m)
-
-mulInteger : Integer → Integer → Integer
-mulInteger (pos    n) (pos    m) = pos (mulNat n m)
-mulInteger (pos    n) (negsuc m) = negNat (mulNat n (suc m))
-mulInteger (negsuc n) (pos    m) = negNat (mulNat (suc n) m)
-mulInteger (negsuc n) (negsuc m) = pos (mulNat (suc n) (suc m))
-
-absInteger : Integer → Integer
-absInteger (pos    n) = pos n
-absInteger (negsuc n) = pos (suc n)
-
-signInteger : Integer → Integer
-signInteger (pos 0)       = 0
-signInteger (pos (suc _)) = 1
-signInteger (negsuc _)    = -1
-
-
---------------------------------------------------
--- Comparisons
-
-eqInteger : Integer → Integer → Bool
-eqInteger (pos n)    (pos m)    = eqNat n m
-eqInteger (negsuc n) (negsuc m) = eqNat n m
-eqInteger _          _          = False
-
-ltInteger : Integer → Integer → Bool
-ltInteger (pos    n) (pos    m) = ltNat n m
-ltInteger (pos    n) (negsuc _) = False
-ltInteger (negsuc n) (pos    _) = True
-ltInteger (negsuc n) (negsuc m) = ltNat m n
-
-
---------------------------------------------------
--- Show
-
-showInteger : Integer → List Char
-showInteger n = primStringToList (primShowInteger n)
-
-
---------------------------------------------------
--- Constraints
-
-isNegativeInteger : Integer → Bool
-isNegativeInteger (pos _)    = False
-isNegativeInteger (negsuc _) = True
-
-IsNonNegativeInteger : Integer → Set
-IsNonNegativeInteger (pos _)      = ⊤
-IsNonNegativeInteger n@(negsuc _) =
-  TypeError (primStringAppend (primShowInteger n) (" is negative"))
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.List.html b/lib/Haskell.Prim.List.html deleted file mode 100644 index 125d797d..00000000 --- a/lib/Haskell.Prim.List.html +++ /dev/null @@ -1,130 +0,0 @@ - -Haskell.Prim.List
-module Haskell.Prim.List where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Int
-
-
---------------------------------------------------
--- List
-
-map : (a → b) → List a → List b
-map f []       = []
-map f (x ∷ xs) = f x ∷ map f xs
-
-infixr 5 _++_
-_++_ : ∀ {@0 ℓ} {@0 a : Set ℓ} → List a → List a → List a
-[]       ++ ys = ys
-(x ∷ xs) ++ ys = x ∷ xs ++ ys
-
-filter : (a → Bool) → List a → List a
-filter p []       = []
-filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs
-
-scanl : (b → a → b) → b → List a → List b
-scanl f z []       = z ∷ []
-scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs
-
-scanr : (a → b → b) → b → List a → List b
-scanr f z [] = z ∷ []
-scanr f z (x ∷ xs) =
-  case scanr f z xs of λ where
-    []         → [] -- impossible
-    qs@(q ∷ _) → f x q ∷ qs
-
-scanl1 : (a → a → a) → List a → List a
-scanl1 f []       = []
-scanl1 f (x ∷ xs) = scanl f x xs
-
-scanr1 : (a → a → a) → List a → List a
-scanr1 f []       = []
-scanr1 f (x ∷ []) = x ∷ []
-scanr1 f (x ∷ xs) =
-  case scanr1 f xs of λ where
-    []         → [] -- impossible
-    qs@(q ∷ _) → f x q ∷ qs
-
-takeWhile : (a → Bool) → List a → List a
-takeWhile p [] = []
-takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else []
-
-dropWhile : (a → Bool) → List a → List a
-dropWhile p [] = []
-dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs
-
-span : (a → Bool) → List a → List a × List a
-span p [] = [] , []
-span p (x ∷ xs) = if p x then first (x ∷_) (span p xs)
-                         else ([] , x ∷ xs)
-
-break : (a → Bool) → List a → List a × List a
-break p = span (not ∘ p)
-
-zipWith : (a → b → c) → List a → List b → List c
-zipWith f []       _        = []
-zipWith f _        []       = []
-zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
-
-zip : List a → List b → List (a × b)
-zip = zipWith _,_
-
-zipWith3 : (a → b → c → d) → List a → List b → List c → List d
-zipWith3 f []       _        _        = []
-zipWith3 f _        []       _        = []
-zipWith3 f _        _        []       = []
-zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs
-
-zip3 : List a → List b → List c → List (a × b × c)
-zip3 = zipWith3 _,_,_
-
-unzip : List (a × b) → List a × List b
-unzip []              = [] , []
-unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys
-
-unzip3 : List (a × b × c) → List a × List b × List c
-unzip3 []                   = [] , [] , []
-unzip3 ((x , y , z) ∷ xyzs) =
-  case unzip3 xyzs of λ where
-    (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs
-
-takeNat : Nat → List a → List a
-takeNat n       [] = []
-takeNat zero    xs = []
-takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs
-
-take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
-take n xs = takeNat (intToNat n) xs
-
-dropNat : Nat → List a → List a
-dropNat n       [] = []
-dropNat zero    xs = xs
-dropNat (suc n) (_ ∷ xs) = dropNat n xs
-
-drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
-drop n xs = dropNat (intToNat n) xs
-
-splitAtNat : (n : Nat) → List a → List a × List a
-splitAtNat _       []       = [] , []
-splitAtNat 0       xs       = [] , xs
-splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs)
-
-splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
-splitAt n xs = splitAtNat (intToNat n) xs
-
-head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
-head (x ∷ _) = x
-
-tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
-tail (_ ∷ xs) = xs
-
-last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
-last (x ∷ [])         = x
-last (_ ∷ xs@(_ ∷ _)) = last xs
-
-init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
-init (x ∷ [])         = []
-init (x ∷ xs@(_ ∷ _)) = x ∷ init xs
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Maybe.html b/lib/Haskell.Prim.Maybe.html deleted file mode 100644 index e0cd83ca..00000000 --- a/lib/Haskell.Prim.Maybe.html +++ /dev/null @@ -1,19 +0,0 @@ - -Haskell.Prim.Maybe
-module Haskell.Prim.Maybe where
-
---------------------------------------------------
--- Maybe
-
-data Maybe {@0 ℓ} (a : Set ℓ) : Set ℓ where
-  Nothing : Maybe a
-  Just    : a -> Maybe a
-
-maybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂} → b → (a → b) → Maybe a → b
-maybe n j Nothing  = n
-maybe n j (Just x) = j x
-
-fromMaybe : {a : Set} → a → Maybe a → a
-fromMaybe d Nothing = d
-fromMaybe _ (Just x) = x
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Monad.html b/lib/Haskell.Prim.Monad.html deleted file mode 100644 index 9fce4388..00000000 --- a/lib/Haskell.Prim.Monad.html +++ /dev/null @@ -1,113 +0,0 @@ - -Haskell.Prim.Monad
-module Haskell.Prim.Monad where
-
-open import Haskell.Prim
-open import Haskell.Prim.Applicative
-open import Haskell.Prim.Either
-open import Haskell.Prim.Foldable
-open import Haskell.Prim.Functor
-open import Haskell.Prim.IO
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Monoid
-open import Haskell.Prim.String
-open import Haskell.Prim.Tuple
-
---------------------------------------------------
--- Monad
-
-module Do where
-
-  -- ** base
-  record Monad (m : Set → Set) : Set₁ where
-    field
-      _>>=_ : m a → (a → m b) → m b
-      overlap ⦃ super ⦄ : Applicative m
-      return : a → m a
-      _>>_ : m a → (@0 {{ a }} → m b) → m b
-      _=<<_ : (a → m b) → m a → m b
-  -- ** defaults
-  record DefaultMonad (m : Set → Set) : Set₁ where
-    field
-      _>>=_ : m a → (a → m b) → m b
-      overlap ⦃ super ⦄ : Applicative m
-    return : a → m a
-    return = pure
-
-    _>>_ : m a → (@0 {{ a }} → m b) → m b
-    m >> m₁ = m >>= λ x → m₁ {{x}}
-
-    _=<<_ : (a → m b) → m a → m b
-    _=<<_ = flip _>>=_
-  -- ** export
-  open Monad ⦃...⦄ public
-  {-# COMPILE AGDA2HS Monad existing-class #-}
-
--- Use `Dont._>>=_` and `Dont._>>_` if you do not want agda2hs to use
--- do-notation.
-module Dont where
-
-  open Do using (Monad)
-
-  _>>=_ : ⦃ Monad m ⦄ → m a → (a → m b) → m b
-  _>>=_ = Do._>>=_
-
-  _>>_ : ⦃ Monad m ⦄ → m a → (@0 {{ a }} → m b) → m b
-  _>>_ = Do._>>_
-
-open Do public
-
-mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤
-mapM₋ f = foldr (λ x k → f x >> k) (pure tt)
-
-sequence₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → t (m a) → m ⊤
-sequence₋ = foldr (λ mx my → mx >> my) (pure tt)
-
--- ** instances
-private
-  mkMonad : DefaultMonad t → Monad t
-  mkMonad x = record {DefaultMonad x}
-
-  infix 0 bind=_
-  bind=_ : ⦃ Applicative m ⦄ → (∀ {a b} → m a → (a → m b) → m b) → Monad m
-  bind= x = record {DefaultMonad (record {_>>=_ = x})}
-instance
-  iMonadList : Monad List
-  iMonadList = bind= flip concatMap
-
-  iMonadMaybe : Monad Maybe
-  iMonadMaybe = bind= flip (maybe Nothing)
-
-  iMonadEither : Monad (Either a)
-  iMonadEither = bind= flip (either Left)
-
-  iMonadFun : Monad (λ b → a → b)
-  iMonadFun = bind= λ f k r → k (f r) r
-
-  iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
-  iMonadTuple₂ = bind= λ (a , x) k → first (a <>_) (k x)
-
-  iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
-  iMonadTuple₃ = bind= λ where
-    (a , b , x) k → case k x of λ where
-      (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y
-
-instance postulate iMonadIO : Monad IO
-
-record MonadFail (m : Set → Set) : Set₁ where
-  field
-    fail : String → m a
-    overlap ⦃ super ⦄ : Monad m
-
-open MonadFail ⦃...⦄ public
-
-{-# COMPILE AGDA2HS MonadFail existing-class #-}
-
-instance
-  MonadFailList : MonadFail List
-  MonadFailList .fail _ = []
-
-  MonadFailMaybe : MonadFail Maybe
-  MonadFailMaybe .fail _ = Nothing
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Monoid.html b/lib/Haskell.Prim.Monoid.html deleted file mode 100644 index bea7e146..00000000 --- a/lib/Haskell.Prim.Monoid.html +++ /dev/null @@ -1,121 +0,0 @@ - -Haskell.Prim.Monoid
-module Haskell.Prim.Monoid where
-
-open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
-open import Haskell.Prim.Tuple
-
---------------------------------------------------
--- Semigroup
-
-record Semigroup (a : Set) : Set where
-  infixr 6 _<>_
-  field _<>_ : a → a → a
-open Semigroup ⦃...⦄ public
-{-# COMPILE AGDA2HS Semigroup existing-class #-}
-
-instance
-  iSemigroupList : Semigroup (List a)
-  iSemigroupList ._<>_ = _++_
-
-  iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
-  iSemigroupMaybe ._<>_          Nothing m = m
-  iSemigroupMaybe ._<>_ m        Nothing   = m
-  iSemigroupMaybe ._<>_ (Just x) (Just y)  = Just (x <> y)
-
-  iSemigroupEither : Semigroup (Either a b)
-  iSemigroupEither ._<>_ (Left _) e = e
-  iSemigroupEither ._<>_ e        _ = e
-
-  iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
-  iSemigroupFun ._<>_ f g x = f x <> g x
-
-  iSemigroupUnit : Semigroup ⊤
-  iSemigroupUnit ._<>_ _ _ = tt
-
-
-  iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b)
-  iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂
-
-  iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c)
-  iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂
-
-
---------------------------------------------------
--- Monoid
-
--- ** base
-record Monoid (a : Set) : Set where
-  field
-    mempty : a
-    overlap ⦃ super ⦄ : Semigroup a
-    mappend : a → a → a
-    mconcat : List a → a
--- ** defaults
-record DefaultMonoid (a : Set) : Set where
-  field
-    mempty : a
-    overlap ⦃ super ⦄ : Semigroup a
-
-  mappend : a → a → a
-  mappend = _<>_
-
-  mconcat : List a → a
-  mconcat []       = mempty
-  mconcat (x ∷ xs) = x <> mconcat xs
--- ** export
-open Monoid ⦃...⦄ public
-{-# COMPILE AGDA2HS Monoid existing-class #-}
--- ** instances
-private
-  infix 0 mempty=_
-  mempty=_ : ⦃ Semigroup a ⦄ → a → Monoid a
-  mempty= x = record {DefaultMonoid (record {mempty = x})}
-
-  mkMonoid : DefaultMonoid a → Monoid a
-  mkMonoid x = record {DefaultMonoid x}
-instance
-  iMonoidList : Monoid (List a)
-  iMonoidList = mempty= []
-
-  iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
-  iMonoidMaybe = mempty= Nothing
-
-  iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
-  iMonoidFun = mempty= λ _ → mempty
-
-  iMonoidUnit : Monoid ⊤
-  iMonoidUnit = mempty= tt
-
-  iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b)
-  iMonoidTuple₂ = mempty= (mempty , mempty)
-
-  iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →  Monoid (a × b × c)
-  iMonoidTuple₃ = mempty= (mempty , mempty , mempty)
-
-open DefaultMonoid
-
-MonoidEndo : Monoid (a → a)
-MonoidEndo = mkMonoid λ where
-  .mempty → id
-  .super ._<>_ → _∘_
-
-MonoidEndoᵒᵖ : Monoid (a → a)
-MonoidEndoᵒᵖ = mkMonoid λ where
-  .mempty      → id
-  .super ._<>_ → flip _∘_
-
-MonoidConj : Monoid Bool
-MonoidConj = mkMonoid λ where
-  .mempty      → True
-  .super ._<>_ → _&&_
-
-MonoidDisj : Monoid Bool
-MonoidDisj = mkMonoid λ where
-  .mempty      → False
-  .super ._<>_ → _||_
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Num.html b/lib/Haskell.Prim.Num.html deleted file mode 100644 index dc1fb841..00000000 --- a/lib/Haskell.Prim.Num.html +++ /dev/null @@ -1,122 +0,0 @@ - -Haskell.Prim.Num
{-# OPTIONS --no-auto-inline #-}
-
-module Haskell.Prim.Num where
-
-open import Haskell.Prim
-open import Haskell.Prim.Word
-open import Haskell.Prim.Int
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Double
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Ord
-open import Haskell.Prim.Monoid
-
---------------------------------------------------
--- Num
-
-record Num (a : Set) : Set₁ where
-  infixl 6 _+_ _-_
-  infixl 7 _*_
-  field
-    @0 MinusOK       : a → a → Set
-    @0 NegateOK      : a → Set
-    @0 FromIntegerOK : Integer → Set
-    _+_           : a → a → a
-    _-_           : (x y : a) → @0 ⦃ MinusOK x y ⦄ → a
-    _*_           : a → a → a
-    negate        : (x : a) → @0 ⦃ NegateOK x ⦄ → a
-    abs           : a → a
-    signum        : a → a
-    fromInteger   : (n : Integer) → @0 ⦃ FromIntegerOK n ⦄ → a
-    overlap ⦃ number ⦄  : Number a
-    overlap ⦃ numZero ⦄ : number .Number.Constraint 0
-    overlap ⦃ numOne ⦄  : number .Number.Constraint 1
-
-open Num ⦃...⦄ public hiding (FromIntegerOK; number)
-
-{-# COMPILE AGDA2HS Num existing-class #-}
-
-instance
-  iNumNat : Num Nat
-  iNumNat .MinusOK n m      = IsFalse (ltNat n m)
-  iNumNat .NegateOK 0       = ⊤
-  iNumNat .NegateOK (suc _) = ⊥
-  iNumNat .Num.FromIntegerOK (negsuc _) = ⊥
-  iNumNat .Num.FromIntegerOK (pos _) = ⊤
-  iNumNat ._+_ n m = addNat n m
-  iNumNat ._-_ n m = monusNat n m
-  iNumNat ._*_ n m = mulNat n m
-  iNumNat .negate n = n
-  iNumNat .abs    n = n
-  iNumNat .signum 0       = 0
-  iNumNat .signum (suc n) = 1
-  iNumNat .fromInteger (pos n) = n
-  iNumNat .fromInteger (negsuc _) ⦃ () ⦄
-
-  iNumInt : Num Int
-  iNumInt .MinusOK _ _         = ⊤
-  iNumInt .NegateOK _          = ⊤
-  iNumInt .Num.FromIntegerOK _ = ⊤
-  iNumInt ._+_ x y             = addInt x y
-  iNumInt ._-_ x y             = subInt x y
-  iNumInt ._*_ x y             = mulInt x y
-  iNumInt .negate x            = negateInt x
-  iNumInt .abs x               = absInt x
-  iNumInt .signum x            = signInt x
-  iNumInt .fromInteger n       = integerToInt n
-
-  iNumInteger : Num Integer
-  iNumInteger .MinusOK _ _ = ⊤
-  iNumInteger .NegateOK _          = ⊤
-  iNumInteger .Num.FromIntegerOK _ = ⊤
-  iNumInteger ._+_ x y             = addInteger x y
-  iNumInteger ._-_ x y             = subInteger x y
-  iNumInteger ._*_ x y             = mulInteger x y
-  iNumInteger .negate x            = negateInteger x
-  iNumInteger .abs x               = absInteger x
-  iNumInteger .signum x            = signInteger x
-  iNumInteger .fromInteger n       = n
-
-  iNumWord : Num Word
-  iNumWord .MinusOK _ _         = ⊤
-  iNumWord .NegateOK _          = ⊤
-  iNumWord .Num.FromIntegerOK _ = ⊤
-  iNumWord ._+_ x y             = addWord x y
-  iNumWord ._-_ x y             = subWord x y
-  iNumWord ._*_ x y             = mulWord x y
-  iNumWord .negate x            = negateWord x
-  iNumWord .abs x               = x
-  iNumWord .signum x            = if x == 0 then 0 else 1
-  iNumWord .fromInteger n       = integerToWord n
-
-  iNumDouble : Num Double
-  iNumDouble .MinusOK _ _         = ⊤
-  iNumDouble .NegateOK _          = ⊤
-  iNumDouble .Num.FromIntegerOK _ = ⊤
-  iNumDouble ._+_ x y             = primFloatPlus x y
-  iNumDouble ._-_ x y             = primFloatMinus x y
-  iNumDouble ._*_ x y             = primFloatTimes x y
-  iNumDouble .negate x            = primFloatMinus 0.0 x
-  iNumDouble .abs x               = if x < 0.0 then primFloatMinus 0.0 x else x
-  iNumDouble .signum x            = case compare x 0.0 of λ where
-                                      LT → -1.0
-                                      EQ → x
-                                      GT → 1.0
-  iNumDouble .fromInteger (pos    n) = fromNat n
-  iNumDouble .fromInteger (negsuc n) = fromNeg (suc n)
-
-open DefaultMonoid
-
-MonoidSum : ⦃ iNum : Num a ⦄ → Monoid a
-MonoidSum = record {DefaultMonoid (λ where
-  .mempty      → 0
-  .super ._<>_ → _+_
- )}
-
-MonoidProduct : ⦃ iNum : Num a ⦄ → Monoid a
-MonoidProduct = record {DefaultMonoid (λ where
-  .mempty      → 1
-  .super ._<>_ → _*_
- )}
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Ord.html b/lib/Haskell.Prim.Ord.html deleted file mode 100644 index 0c8f6d89..00000000 --- a/lib/Haskell.Prim.Ord.html +++ /dev/null @@ -1,173 +0,0 @@ - -Haskell.Prim.Ord
-module Haskell.Prim.Ord where
-
-open import Haskell.Prim
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Int
-open import Haskell.Prim.Word
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Double
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Monoid
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
-
---------------------------------------------------
--- Ordering
-
-data Ordering : Set where
-  LT EQ GT : Ordering
-
-instance
-  iEqOrdering : Eq Ordering
-  iEqOrdering ._==_ LT LT = True
-  iEqOrdering ._==_ EQ EQ = True
-  iEqOrdering ._==_ GT GT = True
-  iEqOrdering ._==_ _  _  = False
-
-  iSemigroupOrdering : Semigroup Ordering
-  iSemigroupOrdering ._<>_ LT _ = LT
-  iSemigroupOrdering ._<>_ EQ o = o
-  iSemigroupOrdering ._<>_ GT _ = GT
-
-  iMonoidOrdering : Monoid Ordering
-  iMonoidOrdering = record {DefaultMonoid (record {mempty = EQ})}
-
---------------------------------------------------
--- Ord
-
-record Ord (a : Set) : Set where
-  field
-    compare : a → a → Ordering
-    _<_  : a → a → Bool
-    _>_  : a → a → Bool
-    _>=_ : a → a → Bool
-    _<=_ : a → a → Bool
-    max  : a → a → a
-    min  : a → a → a
-    overlap ⦃ super ⦄ : Eq a
-
-  infix 4 _<_ _>_ _<=_ _>=_
-
-open Ord ⦃...⦄ public
-
-{-# COMPILE AGDA2HS Ord existing-class #-}
-
-ordFromCompare : ⦃ Eq a ⦄ → (a → a → Ordering) → Ord a
-ordFromCompare cmp .compare = cmp
-ordFromCompare cmp ._<_  x y = cmp x y == LT
-ordFromCompare cmp ._>_  x y = cmp x y == GT
-ordFromCompare cmp ._<=_ x y = cmp x y /= GT
-ordFromCompare cmp ._>=_ x y = cmp x y /= LT
-ordFromCompare cmp .max  x y = if cmp x y == LT then y else x
-ordFromCompare cmp .min  x y = if cmp x y == GT then y else x
-
-ordFromLessThan : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
-ordFromLessThan _<_ .compare x y = if x < y then LT else if x == y then EQ else GT
-ordFromLessThan _<_ ._<_  x y = x < y
-ordFromLessThan _<_ ._>_  x y = y < x
-ordFromLessThan _<_ ._<=_ x y = x < y || x == y
-ordFromLessThan _<_ ._>=_ x y = y < x || x == y
-ordFromLessThan _<_ .max  x y = if x < y then y else x
-ordFromLessThan _<_ .min  x y = if y < x then y else x
-
-ordFromLessEq : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
-ordFromLessEq _<=_ .compare x y = if x == y then EQ else if x <= y then LT else GT
-ordFromLessEq _<=_ ._<_  x y = x <= y && not (x == y)
-ordFromLessEq _<=_ ._>_  x y = y <= x && not (x == y)
-ordFromLessEq _<=_ ._<=_ x y = x <= y
-ordFromLessEq _<=_ ._>=_ x y = y <= x
-ordFromLessEq _<=_ .max  x y = if y <= x then x else y
-ordFromLessEq _<=_ .min  x y = if x <= y then x else y
-
-private
-  compareFromLt : ⦃ Eq a ⦄ → (a → a → Bool) → a → a → Ordering
-  compareFromLt _<_ x y = if x < y then LT else if x == y then EQ else GT
-
-private
-  maxNat : Nat → Nat → Nat
-  maxNat zero    y       = y
-  maxNat (suc x) zero    = suc x
-  maxNat (suc x) (suc y) = suc (maxNat x y)
-
-  minNat : Nat → Nat → Nat
-  minNat zero    y       = zero
-  minNat (suc x) zero    = zero
-  minNat (suc x) (suc y) = suc (minNat x y)
-
-instance
-  iOrdNat : Ord Nat
-  iOrdNat = record (ordFromLessThan ltNat)
-    { max = maxNat
-    ; min = minNat
-    }
-
-  iOrdInteger : Ord Integer
-  iOrdInteger = ordFromLessThan ltInteger
-
-  iOrdInt : Ord Int
-  iOrdInt = ordFromLessThan ltInt
-
-  iOrdWord : Ord Word
-  iOrdWord = ordFromLessThan ltWord
-
-  iOrdDouble : Ord Double
-  iOrdDouble = ordFromLessThan primFloatLess
-
-  iOrdChar : Ord Char
-  iOrdChar = ordFromLessThan λ x y → c2n x < c2n y
-
-  iOrdBool : Ord Bool
-  iOrdBool = ordFromCompare λ where
-    False True  → LT
-    True  False → GT
-    _     _     → EQ
-
-  iOrdUnit : Ord ⊤
-  iOrdUnit = ordFromCompare λ _ _ → EQ
-
-  iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
-  iOrdTuple₂ = ordFromCompare λ where
-    (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂
-
-  iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
-  iOrdTuple₃ = ordFromCompare λ where
-    (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂
-
-compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
-compareList []       []       = EQ
-compareList []       (_ ∷ _)  = LT
-compareList (_ ∷ _)  []       = GT
-compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys
-
-instance
-  iOrdList : ⦃ Ord a ⦄ → Ord (List a)
-  iOrdList = ordFromCompare compareList
-
-  iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
-  iOrdMaybe = ordFromCompare λ where
-    Nothing  Nothing  → EQ
-    Nothing  (Just _) → LT
-    (Just _) Nothing  → GT
-    (Just x) (Just y) → compare x y
-
-  iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
-  iOrdEither = ordFromCompare λ where
-    (Left  x) (Left  y) → compare x y
-    (Left  _) (Right _) → LT
-    (Right _) (Left  _) → GT
-    (Right x) (Right y) → compare x y
-
-  iOrdOrdering : Ord Ordering
-  iOrdOrdering = ordFromCompare λ where
-    LT LT → EQ
-    LT _  → LT
-    _  LT → GT
-    EQ EQ → EQ
-    EQ GT → LT
-    GT EQ → GT
-    GT GT → EQ
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Show.html b/lib/Haskell.Prim.Show.html deleted file mode 100644 index d3525f36..00000000 --- a/lib/Haskell.Prim.Show.html +++ /dev/null @@ -1,130 +0,0 @@ - -Haskell.Prim.Show
-module Haskell.Prim.Show where
-
-open import Haskell.Prim
-open import Haskell.Prim.String
-open import Haskell.Prim.List
-open import Haskell.Prim.Word
-open import Haskell.Prim.Double
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Ord
-open import Haskell.Prim.Either
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Int
-open import Haskell.Prim.Foldable
-
-
---------------------------------------------------
--- Show
-
-ShowS : Set
-ShowS = String → String
-
-showChar : Char → ShowS
-showChar = _∷_
-
-showString : String → ShowS
-showString = _++_
-
-showParen : Bool → ShowS → ShowS
-showParen False s = s
-showParen True  s = showString "(" ∘ s ∘ showString ")"
-
-defaultShowList : (a → ShowS) → List a → ShowS
-defaultShowList shows = λ where
-  []       → showString "[]"
-  (x ∷ xs) → showString "["
-           ∘ foldl (λ s x → s ∘ showString "," ∘ shows x) (shows x) xs
-           ∘ showString "]"
-
--- ** base
-record Show (a : Set) : Set where
-  field
-    showsPrec : Int → a → ShowS
-    showList  : List a → ShowS
-    show      : a → String
--- ** export
-record Show₁ (a : Set) : Set where
-  field showsPrec : Int → a → ShowS
-
-  show : a → String
-  show x = showsPrec 0 x ""
-
-  showList : List a → ShowS
-  showList = defaultShowList (showsPrec 0)
-record Show₂ (a : Set) : Set where
-  field show : a → String
-
-  showsPrec : Int → a → ShowS
-  showsPrec _ x s = show x ++ s
-
-  showList : List a → ShowS
-  showList = defaultShowList (showsPrec 0)
--- ** export
-open Show ⦃...⦄ public
-
-shows : ⦃ Show a ⦄ → a → ShowS
-shows = showsPrec 0
-
-{-# COMPILE AGDA2HS Show existing-class #-}
--- ** instances
-private
-  infix 0 showsPrec=_ show=_
-
-  showsPrec=_ : (Int → a → ShowS) → Show a
-  showsPrec=_ x = record {Show₁ (record {showsPrec = x})}
-
-  show=_ : (a → String) → Show a
-  show= x = record {Show₂ (record {show = x})}
-instance
-  iShowNat : Show Nat
-  iShowNat = show= (primStringToList ∘ primShowNat)
-
-  iShowInteger : Show Integer
-  iShowInteger = show= showInteger
-
-  iShowInt : Show Int
-  iShowInt = show= showInt
-
-  iShowWord : Show Word
-  iShowWord = show= showWord
-
-  iShowDouble : Show Double
-  iShowDouble = show= (primStringToList ∘ primShowFloat)
-
-  iShowBool : Show Bool
-  iShowBool = show= λ where False → "False"; True → "True"
-
-  iShowChar : Show Char
-  iShowChar = showsPrec= λ _ → showString ∘ primStringToList ∘ primShowChar
-
-  iShowList : ⦃ Show a ⦄ → Show (List a)
-  iShowList = showsPrec= λ _ → showList
-private
-  showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS
-  showApp₁ p tag x = showParen (p > 10) $
-    showString tag ∘ showString " " ∘ showsPrec 11 x
-instance
-  iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
-  iShowMaybe = showsPrec= λ where
-    p Nothing  → showString "Nothing"
-    p (Just x) → showApp₁ p "Just" x
-
-  iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b)
-  iShowEither = showsPrec= λ where
-    p (Left  x) → showApp₁ p "Left"  x
-    p (Right y) → showApp₁ p "Right" y
-
-instance
-  iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b)
-  iShowTuple₂ = showsPrec= λ _ → λ where
-    (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")"
-
-  iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c)
-  iShowTuple₃ = showsPrec= λ _ → λ where
-    (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")"
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.String.html b/lib/Haskell.Prim.String.html deleted file mode 100644 index a8ce00a4..00000000 --- a/lib/Haskell.Prim.String.html +++ /dev/null @@ -1,54 +0,0 @@ - -Haskell.Prim.String
-module Haskell.Prim.String where
-
-open import Haskell.Prim
-open import Haskell.Prim.List
-open import Haskell.Prim.Foldable
-
---------------------------------------------------
--- String
--- This is _not_ the builtin String type of Agda
--- which is defined by postulates.
--- `fromString` can be used to convert back
--- to builtin Agda strings.
-
-String = List Char
-
-instance
-  iIsStringString : IsString String
-  iIsStringString .IsString.Constraint _ = ⊤
-  iIsStringString .fromString s = primStringToList s
-
-private
-  cons : Char → List String → List String
-  cons c []       = (c ∷ []) ∷ []
-  cons c (s ∷ ss) = (c ∷ s) ∷ ss
-
-lines : String → List String
-lines []         = []
-lines ('\n' ∷ s) = [] ∷ lines s
-lines (c    ∷ s) = cons c (lines s)
-
-private
- mutual
-  space : String → List String
-  space [] = []
-  space (c ∷ s) = if primIsSpace c then space s else cons c (word s)
-
-  word  : String → List String
-  word []      = []
-  word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s)
-
-words : String → List String
-words [] = []
-words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s
-
-unlines : List String → String
-unlines = concatMap (_++ "\n")
-
-unwords : List String → String
-unwords [] = ""
-unwords (w ∷ []) = w
-unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Traversable.html b/lib/Haskell.Prim.Traversable.html deleted file mode 100644 index 39ce793e..00000000 --- a/lib/Haskell.Prim.Traversable.html +++ /dev/null @@ -1,80 +0,0 @@ - -Haskell.Prim.Traversable
-
-module Haskell.Prim.Traversable where
-
-open import Haskell.Prim
-open import Haskell.Prim.Applicative
-open import Haskell.Prim.Functor
-open import Haskell.Prim.Foldable
-open import Haskell.Prim.Monad
-open import Haskell.Prim.List
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
-open import Haskell.Prim.Tuple
-
---------------------------------------------------
--- Traversable
-
--- ** base
-record Traversable (t : Set → Set) : Set₁ where
-  field
-    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
-    overlap ⦃ functor ⦄ : Functor t
-    overlap ⦃ foldable ⦄ : Foldable t
-
-    sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
-    mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
-    sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
--- ** defaults
-record DefaultTraversable (t : Set → Set) : Set₁ where
-  field
-    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
-    overlap ⦃ functor ⦄ : Functor t
-    overlap ⦃ foldable ⦄ : Foldable t
-
-  sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
-  sequenceA = traverse id
-
-  mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
-  mapM = traverse
-
-  sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
-  sequence = sequenceA
--- ** export
-open Traversable ⦃...⦄ public
-{-# COMPILE AGDA2HS Traversable existing-class #-}
--- ** instances
-private
-  mkTraversable : DefaultTraversable t → Traversable t
-  mkTraversable x = record {DefaultTraversable x}
-
-  infix 0 traverse=_
-  traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄
-            → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b))
-            → Traversable t
-  traverse= x = record {DefaultTraversable (record {traverse = x})}
-instance
-  open DefaultTraversable
-
-  iTraversableList : Traversable List
-  iTraversableList = traverse= traverseList
-    where
-      traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b)
-      traverseList f []       = pure []
-      traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈
-
-  iTraversableMaybe : Traversable Maybe
-  iTraversableMaybe = traverse= λ where
-    f Nothing  → pure Nothing
-    f (Just x) → Just <$> f x
-
-  iTraversableEither : Traversable (Either a)
-  iTraversableEither = traverse= λ where
-    f (Left  x) → pure (Left x)
-    f (Right y) → Right <$> f y
-
-  iTraversablePair : Traversable (a ×_)
-  iTraversablePair = traverse= λ
-    f (x , y) → (x ,_) <$> f y
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Tuple.html b/lib/Haskell.Prim.Tuple.html deleted file mode 100644 index 718b3e77..00000000 --- a/lib/Haskell.Prim.Tuple.html +++ /dev/null @@ -1,47 +0,0 @@ - -Haskell.Prim.Tuple
-module Haskell.Prim.Tuple where
-
-open import Haskell.Prim
-
---------------------------------------------------
--- Tuples
-
-infix 3 _×_ _×_×_
-
-infix -1 _,_ _,_,_
-
-record _×_ (a b : Set) : Set where
-  constructor _,_
-  field
-    fst : a
-    snd : b
-open _×_ public
-
-data _×_×_ (a b c : Set) : Set where
-  _,_,_ : a → b → c → a × b × c
-
-uncurry : (a → b → c) → a × b → c
-uncurry f (x , y) = f x y
-
-curry : (a × b → c) → a → b → c
-curry f x y = f (x , y)
-
-first : (a → b) → a × c → b × c
-first f (x , y) = f x , y
-
-second : (a → b) → c × a → c × b
-second f (x , y) = x , f y
-
-_***_ : (a → b) → (c → d) → a × c → b × d
-(f *** g) (x , y) = f x , g y
-
-fst₃ : (a × b × c) → a
-fst₃ (x , _ , _) = x 
-
-snd₃ : (a × b × c) → b
-snd₃ (_ , y , _) = y
-
-thd₃ : (a × b × c) → c
-thd₃ (_ , _ , z) = z
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.Word.html b/lib/Haskell.Prim.Word.html deleted file mode 100644 index 2e31aefd..00000000 --- a/lib/Haskell.Prim.Word.html +++ /dev/null @@ -1,56 +0,0 @@ - -Haskell.Prim.Word
-module Haskell.Prim.Word where
-
-open import Haskell.Prim
-open import Haskell.Prim.Integer
-
-import Agda.Builtin.Word renaming (Word64 to Word)
-open Agda.Builtin.Word public using (Word)
-
-
---------------------------------------------------
--- Literals
-
-module WordInternal where
-  2⁶⁴ : Nat
-  2⁶⁴ = 18446744073709551616
-open WordInternal
-
-instance
-  iNumberWord : Number Word
-  iNumberWord .Number.Constraint n = IsTrue (ltNat n 2⁶⁴)
-  iNumberWord .fromNat n = n2w n
-
-
---------------------------------------------------
--- Arithmetic
-
-negateWord : Word → Word
-negateWord a = n2w (monusNat 2⁶⁴ (w2n a))
-
-addWord : Word → Word → Word
-addWord a b = n2w (addNat (w2n a) (w2n b))
-
-subWord : Word → Word → Word
-subWord a b = addWord a (negateWord b)
-
-mulWord : Word → Word → Word
-mulWord a b = n2w (mulNat (w2n a) (w2n b))
-
-eqWord : Word → Word → Bool
-eqWord a b = eqNat (w2n a) (w2n b)
-
-ltWord : Word → Word → Bool
-ltWord a b = ltNat (w2n a) (w2n b)
-
-showWord : Word → List Char
-showWord a = primStringToList (primShowNat (w2n a))
-
-integerToWord : Integer → Word
-integerToWord (pos n)    = n2w n
-integerToWord (negsuc n) = negateWord (n2w (suc n))
-
-wordToInteger : Word → Integer
-wordToInteger n = pos (w2n n)
-
\ No newline at end of file diff --git a/lib/Haskell.Prim.html b/lib/Haskell.Prim.html deleted file mode 100644 index a473fe27..00000000 --- a/lib/Haskell.Prim.html +++ /dev/null @@ -1,132 +0,0 @@ - -Haskell.Prim
{-# OPTIONS --no-auto-inline #-}
-
--- Basic things needed by other primitive modules.
--- Note that this module exports types and functions that should not
--- be used directly in Haskell definitions, so you probably want to
--- import Haskell.Prelude instead.
-
-module Haskell.Prim where
-
-open import Agda.Primitive          public
-open import Agda.Builtin.Bool       public renaming (true to True; false to False)
-open import Agda.Builtin.Int        public renaming (Int to Integer)
-open import Agda.Builtin.Nat        public renaming (_==_ to eqNat; _<_ to ltNat; _+_ to addNat; _-_ to monusNat; _*_ to mulNat)
-open import Agda.Builtin.Char       public renaming (primCharToNat to c2n)
-open import Agda.Builtin.Unit       public
-open import Agda.Builtin.Equality   public
-open import Agda.Builtin.FromString public
-open import Agda.Builtin.FromNat    public
-open import Agda.Builtin.FromNeg    public
-open import Agda.Builtin.String     public renaming (String to AgdaString)
-open import Agda.Builtin.Word       public renaming (primWord64ToNat to w2n; primWord64FromNat to n2w)
-open import Agda.Builtin.Strict     public
-open import Agda.Builtin.List       public
-
-variable
-  @0 ℓ : Level
-  a b c d e : Set
-  f m s t : Set → Set
-
-
---------------------------------------------------
--- Functions
-
-id : a → a
-id x = x
-
-infixr 9 _∘_
-_∘_ : (b → c) → (a → b) → a → c
-(f ∘ g) x = f (g x)
-
-flip : (a → b → c) → b → a → c
-flip f x y = f y x
-
-const : a → b → a
-const x _ = x
-
-infixr 0 _$_
-_$_ : (a → b) → a → b
-f $ x = f x
-
-
---------------------------------------------------
--- Language constructs
-
-infix -1 case_of_
-case_of_ : (a' : a) → ((a'' : a) → @0 {{ a' ≡ a'' }} → b) → b
-case x of f = f x
-
-infix -2 if_then_else_
-if_then_else_ : {@0 a : Set ℓ} → (flg : Bool) → (@0 {{ flg ≡ True }} → a) → (@0 {{ flg ≡ False }} → a) → a
-if False then x else y = y
-if True  then x else y = x
-
--- for explicit type signatures (e. g. `4 :: Integer` is `the Int 4`)
-the : (@0 a : Set ℓ) -> a -> a
-the _ x = x
-
---------------------------------------------------
--- Agda strings
-
-instance
-  iIsStringAgdaString : IsString AgdaString
-  iIsStringAgdaString .IsString.Constraint _ = ⊤
-  iIsStringAgdaString .fromString s = s
-
-
---------------------------------------------------
--- Numbers
-
-instance
-  iNumberNat : Number Nat
-  iNumberNat .Number.Constraint _ = ⊤
-  iNumberNat .fromNat n = n
-
-
---------------------------------------------------
--- Lists
-
-lengthNat : List a → Nat
-lengthNat []       = 0
-lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs)
-
-
---------------------------------------------------
--- Proof things
-
-data ⊥ : Set where
-
-magic : {A : Set} → ⊥ → A
-magic ()
-
---principle of explosion
-exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
-exFalso {False} () b 
-exFalso {True} a ()
-
--- Use to bundle up constraints
-data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
-  instance
-    allNil  : All B []
-    allCons : ∀ {x xs} ⦃ i : B x ⦄ ⦃ is : All B xs ⦄ → All B (x ∷ xs)
-
-data Any {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
-  instance
-    anyHere  : ∀ {x xs} ⦃ i : B x ⦄ → Any B (x ∷ xs)
-    anyThere : ∀ {x xs} ⦃ is : Any B xs ⦄ → Any B (x ∷ xs)
-
-data IsTrue : Bool → Set where
-  instance itsTrue : IsTrue True
-
-data IsFalse : Bool → Set where
-  instance itsFalse : IsFalse False
-
-data NonEmpty {a : Set} : List a → Set where
-  instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
-
-data TypeError (err : AgdaString) : Set where
-
-it : ∀ {@0 ℓ} {@0 a : Set ℓ} → ⦃ a ⦄ → a
-it ⦃ x ⦄ = x
-
\ No newline at end of file diff --git a/lib/index.html b/lib/index.html deleted file mode 100644 index d2f1e269..00000000 --- a/lib/index.html +++ /dev/null @@ -1,144 +0,0 @@ - -Haskell.Prelude
{-# OPTIONS --no-auto-inline #-}
-module Haskell.Prelude where
-
-open import Haskell.Prim
-open Haskell.Prim public using
-  ( Bool; True; False; Char; Integer;
-    List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
-    IsTrue; IsFalse; NonEmpty;
-    All; allNil; allCons;
-    Any; anyHere; anyThere;
-    id; _∘_; _$_; flip; const;
-    if_then_else_; case_of_;
-    Number; fromNat; Negative; fromNeg;
-    IsString; fromString;
-    _≡_; refl;
-    a; b; c; d; e; f; m; s; t )
-
-open import Haskell.Prim.Absurd      public
-open import Haskell.Prim.Applicative public
-open import Haskell.Prim.Bool        public
-open import Haskell.Prim.Bounded     public
-open import Haskell.Prim.Char        public
-open import Haskell.Prim.Double      public
-open import Haskell.Prim.Either      public
-open import Haskell.Prim.Enum        public
-open import Haskell.Prim.Eq          public
-open import Haskell.Prim.Foldable    public
-open import Haskell.Prim.Functor     public
-open import Haskell.Prim.Int         public
-open import Haskell.Prim.Integer     public
-open import Haskell.Prim.IO          public
-open import Haskell.Prim.List        public
-open import Haskell.Prim.Maybe       public
-open import Haskell.Prim.Monad       public
-open import Haskell.Prim.Monoid      public
-open import Haskell.Prim.Num         public
-open import Haskell.Prim.Ord         public
-open import Haskell.Prim.Show        public
-open import Haskell.Prim.String      public
-open import Haskell.Prim.Traversable public
-open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
-open import Haskell.Prim.Word        public
-
--- Problematic features
---  - [Partial]:  Could pass implicit/instance arguments to prove totality.
---  - [Float]:    Or Float (Agda floats are Doubles)
---  - [Infinite]: Define colists and map to Haskell lists?
-
--- Missing from the Haskell Prelude:
---
---     Float        [Float]
---     Rational
---
---     Real(toRational),
---     Integral(quot, rem, div, mod, quotRem, divMod, toInteger),
---     Fractional((/), recip, fromRational),
---     Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,
---              asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),
---     RealFrac(properFraction, truncate, round, ceiling, floor),
---     RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
---               encodeFloat, exponent, significand, scaleFloat, isNaN,
---               isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
---
---     subtract, even, odd, gcd, lcm, (^), (^^),
---     fromIntegral, realToFrac,
---
---     foldr1, foldl1, maximum, minimum      [Partial]
---
---     until [Partial]
---
---     iterate, repeat, cycle          [Infinite]
---
---     ReadS, Read(readsPrec, readList),
---     reads, readParen, read, lex,
---
---     IO, putChar, putStr, putStrLn, print,
---     getChar, getLine, getContents, interact,
---     FilePath, readFile, writeFile, appendFile, readIO, readLn,
---     IOError, ioError, userError,
-
-
---------------------------------------------------
--- Functions
-
-infixr 0 _$!_
-
-_$!_ : (a → b) → a → b
-_$!_ = _$_
-
-seq : a → b → b
-seq = const id
-
-asTypeOf : a → a → a
-asTypeOf x _ = x
-
-undefined : {@0 @(tactic absurd) i : ⊥} → a
-undefined {i = ()}
-
-error : {@0 @(tactic absurd) i : ⊥} → String → a
-error {i = ()} err
-
-errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
-errorWithoutStackTrace {i = ()} err
-
--------------------------------------------------
--- More List functions
---   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
---   turning those dependencies around.
-
-reverse : List a → List a
-reverse = foldl (flip _∷_) []
-
-infixl 9 _!!_ _!!ᴺ_
-
-_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
-(x ∷ xs) !!ᴺ zero  = x
-(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n
-
-_!!_ : (xs : List a) (n : Int)
-     → ⦃ @0 nn : IsNonNegativeInt n ⦄
-     → ⦃ @0 _  : IsTrue (intToNat n {{nn}} < lengthNat xs) ⦄ → a
-xs !! n = xs !!ᴺ intToNat n
-
-lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
-lookup x []              = Nothing
-lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
-
-
--------------------------------------------------
--- Unsafe functions
-
-coerce : @0 a ≡ b → a → b
-coerce refl x = x
-
-IsJust : Maybe a → Set
-IsJust Nothing  = ⊥
-IsJust (Just _) = ⊤
-
-fromJust : (x : Maybe a) → @0 {IsJust x} → a
-fromJust Nothing  = error "fromJust Nothing"
-fromJust (Just x) = x
-
\ No newline at end of file