diff --git a/lib/Agda.Builtin.Bool.html b/lib/Agda.Builtin.Bool.html
new file mode 100644
index 00000000..63da33b2
--- /dev/null
+++ b/lib/Agda.Builtin.Bool.html
@@ -0,0 +1,17 @@
+
+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 #-}
+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
+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 _≡_ #-}
+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
+
+ primFloatInequality : Float → Float → Bool
+ primFloatEquality : Float → Float → Bool
+ primFloatLess : Float → Float → Bool
+ primFloatIsInfinite : Float → Bool
+ primFloatIsNaN : Float → Bool
+ primFloatIsNegativeZero : Float → Bool
+ primFloatIsSafeInteger : Float → Bool
+
+ 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
+
+ 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."
+#-}
+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 #-}
+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 #-}
+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 #-}
+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
+
+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
+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); }; } #-}
+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 #-}
+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 _<_ #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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 #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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 #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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
+
+
+
+postulate Name : Set
+{-# BUILTIN QNAME Name #-}
+
+primitive
+ primQNameEquality : Name → Name → Bool
+ primQNameLess : Name → Name → Bool
+ primShowQName : Name → String
+
+
+
+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 )
+
+
+
+postulate Meta : Set
+{-# BUILTIN AGDAMETA Meta #-}
+
+primitive
+ primMetaEquality : Meta → Meta → Bool
+ primMetaLess : Meta → Meta → Bool
+ primShowMeta : Meta → String
+ primMetaToNat : Meta → Nat
+
+
+
+
+data Visibility : Set where
+ visible hidden instance′ : Visibility
+
+{-# BUILTIN HIDING Visibility #-}
+{-# BUILTIN VISIBLE visible #-}
+{-# BUILTIN HIDDEN hidden #-}
+{-# BUILTIN INSTANCE instance′ #-}
+
+
+data Relevance : Set where
+ relevant irrelevant : Relevance
+
+{-# BUILTIN RELEVANCE Relevance #-}
+{-# BUILTIN RELEVANT relevant #-}
+{-# BUILTIN IRRELEVANT irrelevant #-}
+
+
+data Quantity : Set where
+ quantity-0 quantity-ω : Quantity
+
+{-# BUILTIN QUANTITY Quantity #-}
+{-# BUILTIN QUANTITY-0 quantity-0 #-}
+{-# BUILTIN QUANTITY-ω quantity-ω #-}
+
+
+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 #-}
+
+
+
+data Abs { a } ( A : Set a ) : Set a where
+ abs : ( s : String ) ( x : A ) → Abs A
+
+{-# BUILTIN ABS Abs #-}
+{-# BUILTIN ABSABS abs #-}
+
+
+
+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 #-}
+
+
+
+
+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
+
+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 #-}
+
+
+
+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 #-}
+
+
+
+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 #-}
+
+
+
+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 ⊤
+
+
+
+ withNormalisation : ∀ { a } { A : Set a } → Bool → TC A → TC A
+ askNormalisation : TC Bool
+
+
+
+ withReconstructed : ∀ { a } { A : Set a } → Bool → TC A → TC A
+ askReconstructed : TC Bool
+
+
+ withExpandLast : ∀ { a } { A : Set a } → Bool → TC A → TC A
+ askExpandLast : TC Bool
+
+
+
+ withReduceDefs : ∀ { a } { A : Set a } → ( Σ Bool λ _ → List Name ) → TC A → TC A
+ askReduceDefs : TC ( Σ Bool λ _ → List Name )
+
+ formatErrorParts : List ErrorPart → TC String
+
+
+ debugPrint : String → Nat → List ErrorPart → TC ⊤
+
+
+
+ noConstraints : ∀ { a } { A : Set a } → TC A → TC A
+
+
+
+
+ runSpeculative : ∀ { a } { A : Set a } → TC ( Σ A λ _ → Bool ) → TC A
+
+
+
+ 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 #-}
+
+
+
+
+{-# 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`" #-}
+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 Σ #-}
+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
+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); } #-}
+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 () (()) #-}
+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
+Agda.Primitive
+
+{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
+
+module Agda.Primitive where
+
+
+
+
+
+infixl 6 _⊔_
+
+{-# BUILTIN PROP Prop #-}
+{-# BUILTIN TYPE Set #-}
+{-# BUILTIN STRICTSET SSet #-}
+
+{-# BUILTIN PROPOMEGA Propω #-}
+{-# BUILTIN SETOMEGA Setω #-}
+{-# BUILTIN STRICTSETOMEGA SSetω #-}
+
+{-# BUILTIN LEVELUNIV LevelUniv #-}
+
+
+
+
+postulate
+ Level : LevelUniv
+
+
+
+
+{-# 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
new file mode 100644
index 00000000..86813a50
--- /dev/null
+++ b/lib/Agda.css
@@ -0,0 +1,41 @@
+/* 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
new file mode 100644
index 00000000..2a76cb63
--- /dev/null
+++ b/lib/Haskell.Prelude.html
@@ -0,0 +1,142 @@
+
+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 ; IsTrue ; IsFalse ;
+ All ; allNil ; allCons ; NonEmpty ; lengthNat ;
+ 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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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
+
+
+
+
+
+
+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
+
+
+
+
+
+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
+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
new file mode 100644
index 00000000..3d84fb89
--- /dev/null
+++ b/lib/Haskell.Prim.Applicative.html
@@ -0,0 +1,85 @@
+
+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
+
+
+
+
+
+
+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
+
+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
+
+open Applicative ⦃...⦄ public
+{-# COMPILE AGDA2HS Applicative existing-class #-}
+
+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
+Haskell.Prim.Bool
+module Haskell.Prim.Bool where
+
+open import Haskell.Prim
+
+
+
+
+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
new file mode 100644
index 00000000..2c8a7de2
--- /dev/null
+++ b/lib/Haskell.Prim.Bounded.html
@@ -0,0 +1,96 @@
+
+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
+
+
+
+
+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
+
+
+
+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
new file mode 100644
index 00000000..5cef9fd6
--- /dev/null
+++ b/lib/Haskell.Prim.Char.html
@@ -0,0 +1,11 @@
+
+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 )
+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
new file mode 100644
index 00000000..0653403d
--- /dev/null
+++ b/lib/Haskell.Prim.Either.html
@@ -0,0 +1,22 @@
+
+Haskell.Prim.Either
+module Haskell.Prim.Either where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+
+
+
+
+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
new file mode 100644
index 00000000..87b67c19
--- /dev/null
+++ b/lib/Haskell.Prim.Enum.html
@@ -0,0 +1,205 @@
+
+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
+
+
+
+
+
+
+
+
+
+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
+
+
+
+
+
+ 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 → []
+ 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 ; _ → '_'
+
+
+
+
\ No newline at end of file
diff --git a/lib/Haskell.Prim.Eq.html b/lib/Haskell.Prim.Eq.html
new file mode 100644
index 00000000..bb73795e
--- /dev/null
+++ b/lib/Haskell.Prim.Eq.html
@@ -0,0 +1,82 @@
+
+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
+
+
+
+
+record Eq ( a : Set ) : Set where
+ infix 4 _==_ _/=_
+ field
+ _==_ : a → a → Bool
+
+ _/=_ : a → a → Bool
+ x /= y = not ( x == y )
+
+open Eq ⦃...⦄ public
+
+{-# COMPILE AGDA2HS Eq existing-class #-}
+
+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
new file mode 100644
index 00000000..c1fa9c6b
--- /dev/null
+++ b/lib/Haskell.Prim.Foldable.html
@@ -0,0 +1,118 @@
+
+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
+
+
+
+
+
+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
+
+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 )
+
+open Foldable ⦃...⦄ public
+{-# COMPILE AGDA2HS Foldable existing-class #-}
+
+
+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
new file mode 100644
index 00000000..e9b93875
--- /dev/null
+++ b/lib/Haskell.Prim.Functor.html
@@ -0,0 +1,81 @@
+
+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
+
+
+
+
+
+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 ⊤
+
+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 <$_
+
+open Functor ⦃...⦄ public
+{-# COMPILE AGDA2HS Functor existing-class #-}
+
+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
new file mode 100644
index 00000000..03f84638
--- /dev/null
+++ b/lib/Haskell.Prim.IO.html
@@ -0,0 +1,29 @@
+
+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
+
+ interact : ( String → String ) → IO ⊤
+ getContents : IO String
+ getLine : IO String
+ getChar : IO Char
+
+
+ print : ⦃ Show a ⦄ → a → IO ⊤
+ putChar : Char → IO ⊤
+ putStr : String → IO ⊤
+ putStrLn : String → IO ⊤
+
+
+ readFile : FilePath → IO String
+ writeFile : FilePath → String → IO ⊤
+ appendFile : FilePath → String → IO ⊤
+Haskell.Prim.Int {-# OPTIONS --no-auto-inline #-}
+
+
+
+
+module Haskell.Prim.Int where
+
+open import Haskell.Prim
+open import Haskell.Prim.Word
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Bool
+
+
+
+
+
+data Int : Set where
+ int64 : Word64 → Int
+
+intToWord : Int → Word64
+intToWord ( int64 a ) = a
+
+unsafeIntToNat : Int → Nat
+unsafeIntToNat a = w2n ( intToWord a )
+
+
+
+
+
+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 ))
+
+
+
+
+
+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 )
+
+
+
+
+
+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
+Haskell.Prim.Integer
+module Haskell.Prim.Integer where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+
+
+
+
+
+private
+ negNat : Nat → Integer
+ negNat 0 = pos 0
+ negNat ( suc n ) = negsuc n
+
+instance
+ iNumberInteger : Number Integer
+ iNumberInteger . Number.Constraint _ = ⊤
+ iNumberInteger . fromNat n = pos n
+
+ iNegativeInteger : Negative Integer
+ iNegativeInteger . Negative.Constraint _ = ⊤
+ iNegativeInteger . fromNeg n = negNat n
+
+
+
+
+
+private
+ subNat : Nat → Nat → Integer
+ subNat n m = if ( ltNat n m ) then negsuc ( monusNat m ( suc n )) else pos ( monusNat n m )
+
+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
+
+
+
+
+
+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
+
+
+
+
+
+showInteger : Integer → List Char
+showInteger n = primStringToList ( primShowInteger n )
+
+
+
+
+
+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
new file mode 100644
index 00000000..a3affb3a
--- /dev/null
+++ b/lib/Haskell.Prim.List.html
@@ -0,0 +1,130 @@
+
+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
+
+
+
+
+
+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
+ [] → []
+ 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
+ [] → []
+ 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
new file mode 100644
index 00000000..e0cd83ca
--- /dev/null
+++ b/lib/Haskell.Prim.Maybe.html
@@ -0,0 +1,19 @@
+
+Haskell.Prim.Maybe
+module Haskell.Prim.Maybe where
+
+
+
+
+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
new file mode 100644
index 00000000..9fce4388
--- /dev/null
+++ b/lib/Haskell.Prim.Monad.html
@@ -0,0 +1,113 @@
+
+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
+
+
+
+
+module Do where
+
+
+ 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
+
+ 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 _>>=_
+
+ open Monad ⦃...⦄ public
+ {-# COMPILE AGDA2HS Monad existing-class #-}
+
+
+
+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 )
+
+
+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
new file mode 100644
index 00000000..bea7e146
--- /dev/null
+++ b/lib/Haskell.Prim.Monoid.html
@@ -0,0 +1,121 @@
+
+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
+
+
+
+
+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₂
+
+
+
+
+
+
+record Monoid ( a : Set ) : Set where
+ field
+ mempty : a
+ overlap ⦃ super ⦄ : Semigroup a
+ mappend : a → a → a
+ mconcat : List a → a
+
+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
+
+open Monoid ⦃...⦄ public
+{-# COMPILE AGDA2HS Monoid existing-class #-}
+
+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
new file mode 100644
index 00000000..7bf86619
--- /dev/null
+++ b/lib/Haskell.Prim.Num.html
@@ -0,0 +1,122 @@
+
+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
+
+
+
+
+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 . _<>_ → _*_
+ )}
+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
+
+
+
+
+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 })}
+
+
+
+
+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
new file mode 100644
index 00000000..42b035b1
--- /dev/null
+++ b/lib/Haskell.Prim.Show.html
@@ -0,0 +1,130 @@
+
+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
+
+
+
+
+
+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 "]"
+
+
+record Show ( a : Set ) : Set where
+ field
+ showsPrec : Int → a → ShowS
+ showList : List a → ShowS
+ show : a → String
+
+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 )
+
+open Show ⦃...⦄ public
+
+shows : ⦃ Show a ⦄ → a → ShowS
+shows = showsPrec 0
+
+{-# COMPILE AGDA2HS Show existing-class #-}
+
+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
new file mode 100644
index 00000000..a8ce00a4
--- /dev/null
+++ b/lib/Haskell.Prim.String.html
@@ -0,0 +1,54 @@
+
+Haskell.Prim.String
+module Haskell.Prim.String where
+
+open import Haskell.Prim
+open import Haskell.Prim.List
+open import Haskell.Prim.Foldable
+
+
+
+
+
+
+
+
+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
new file mode 100644
index 00000000..39ce793e
--- /dev/null
+++ b/lib/Haskell.Prim.Traversable.html
@@ -0,0 +1,80 @@
+
+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
+
+
+
+
+
+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 )
+
+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
+
+open Traversable ⦃...⦄ public
+{-# COMPILE AGDA2HS Traversable existing-class #-}
+
+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
new file mode 100644
index 00000000..718b3e77
--- /dev/null
+++ b/lib/Haskell.Prim.Tuple.html
@@ -0,0 +1,47 @@
+
+Haskell.Prim.Tuple
+module Haskell.Prim.Tuple where
+
+open import Haskell.Prim
+
+
+
+
+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
new file mode 100644
index 00000000..314b5fec
--- /dev/null
+++ b/lib/Haskell.Prim.Word.html
@@ -0,0 +1,55 @@
+
+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 )
+
+
+
+
+
+private
+ 2⁶⁴ : Nat
+ 2⁶⁴ = 18446744073709551616
+
+instance
+ iNumberWord : Number Word
+ iNumberWord . Number.Constraint n = IsTrue ( ltNat n 2⁶⁴ )
+ iNumberWord . fromNat n = n2w n
+
+
+
+
+
+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
new file mode 100644
index 00000000..d0d0b15a
--- /dev/null
+++ b/lib/Haskell.Prim.html
@@ -0,0 +1,127 @@
+
+Haskell.Prim {-# OPTIONS --no-auto-inline #-}
+
+
+
+
+
+
+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
+
+
+
+
+
+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
+
+
+
+
+
+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
+
+
+the : (@ 0 a : Set ℓ ) -> a -> a
+the _ x = x
+
+
+
+
+instance
+ iIsStringAgdaString : IsString AgdaString
+ iIsStringAgdaString . IsString.Constraint _ = ⊤
+ iIsStringAgdaString . fromString s = s
+
+
+
+
+
+instance
+ iNumberNat : Number Nat
+ iNumberNat . Number.Constraint _ = ⊤
+ iNumberNat . fromNat n = n
+
+
+
+
+
+lengthNat : List a → Nat
+lengthNat [] = 0
+lengthNat (_ ∷ xs ) = addNat 1 ( lengthNat xs )
+
+
+
+
+
+data ⊥ : Set where
+
+magic : { A : Set } → ⊥ → A
+magic ()
+
+
+exFalso : { x : Bool } → ( x ≡ True ) → ( x ≡ False ) → ⊥
+exFalso { False } () b
+exFalso { True } a ()
+
+
+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 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
+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 ; IsTrue ; IsFalse ;
+ All ; allNil ; allCons ; NonEmpty ; lengthNat ;
+ 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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+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
+
+
+
+
+
+
+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
+
+
+
+
+
+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
+