dhall-1.26.0: dhall-lang/tests/typecheck/success/preludeB.dhall
{ Bool :
{ and :
∀(xs : List Bool) → Bool
, build :
∀(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
, even :
∀(xs : List Bool) → Bool
, fold :
∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
, not :
∀(b : Bool) → Bool
, odd :
∀(xs : List Bool) → Bool
, or :
∀(xs : List Bool) → Bool
, show :
∀(b : Bool) → Text
}
, Double :
{ show : Double → Text }
, Function :
{ compose :
∀(A : Type)
→ ∀(B : Type)
→ ∀(C : Type)
→ ∀(f : A → B)
→ ∀(g : B → C)
→ ∀(x : A)
→ C
}
, Integer :
{ show : Integer → Text, toDouble : Integer → Double }
, JSON :
{ array :
∀ ( x
: List
( ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
)
)
→ ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
, bool :
∀(x : Bool)
→ ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
, keyText :
∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }
, keyValue :
∀(v : Type)
→ ∀(key : Text)
→ ∀(value : v)
→ { mapKey : Text, mapValue : v }
, null :
∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
, number :
∀(x : Double)
→ ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
, object :
∀ ( x
: List
{ mapKey :
Text
, mapValue :
∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
}
)
→ ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
, render :
∀ ( j
: ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
)
→ Text
, string :
∀(x : Text)
→ ∀(JSON : Type)
→ ∀ ( json
: { array :
List JSON → JSON
, bool :
Bool → JSON
, null :
JSON
, number :
Double → JSON
, object :
List { mapKey : Text, mapValue : JSON } → JSON
, string :
Text → JSON
}
)
→ JSON
}
, List :
{ all :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool
, any :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool
, build :
∀(a : Type)
→ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
→ List a
, concat :
∀(a : Type) → ∀(xss : List (List a)) → List a
, concatMap :
∀(a : Type) → ∀(b : Type) → ∀(f : a → List b) → ∀(xs : List a) → List b
, filter :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a
, fold :
∀(a : Type)
→ List a
→ ∀(list : Type)
→ ∀(cons : a → list → list)
→ ∀(nil : list)
→ list
, generate :
∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a
, head :
∀(a : Type) → List a → Optional a
, indexed :
∀(a : Type) → List a → List { index : Natural, value : a }
, iterate :
∀(n : Natural) → ∀(a : Type) → ∀(f : a → a) → ∀(x : a) → List a
, last :
∀(a : Type) → List a → Optional a
, length :
∀(a : Type) → List a → Natural
, map :
∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b
, null :
∀(a : Type) → ∀(xs : List a) → Bool
, replicate :
∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a
, reverse :
∀(a : Type) → List a → List a
, shifted :
∀(a : Type)
→ ∀(kvss : List (List { index : Natural, value : a }))
→ List { index : Natural, value : a }
, unzip :
∀(a : Type)
→ ∀(b : Type)
→ ∀(xs : List { _1 : a, _2 : b })
→ { _1 : List a, _2 : List b }
}
, Map :
{ keys :
∀(k : Type)
→ ∀(v : Type)
→ ∀(xs : List { mapKey : k, mapValue : v })
→ List k
, map :
∀(k : Type)
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(f : a → b)
→ ∀(m : List { mapKey : k, mapValue : a })
→ List { mapKey : k, mapValue : b }
, values :
∀(k : Type)
→ ∀(v : Type)
→ ∀(xs : List { mapKey : k, mapValue : v })
→ List v
}
, Natural :
{ build :
( ∀(natural : Type)
→ ∀(succ : natural → natural)
→ ∀(zero : natural)
→ natural
)
→ Natural
, enumerate :
∀(n : Natural) → List Natural
, even :
Natural → Bool
, fold :
Natural
→ ∀(natural : Type)
→ ∀(succ : natural → natural)
→ ∀(zero : natural)
→ natural
, isZero :
Natural → Bool
, odd :
Natural → Bool
, product :
∀(xs : List Natural) → Natural
, show :
Natural → Text
, sum :
∀(xs : List Natural) → Natural
, toDouble :
∀(n : Natural) → Double
, toInteger :
Natural → Integer
, lessThan :
Natural → Natural → Bool
, lessThanEqual :
Natural → Natural → Bool
, equal :
Natural → Natural → Bool
, greaterThan :
Natural → Natural → Bool
, greaterThanEqual :
Natural → Natural → Bool
}
, Optional :
{ all :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool
, any :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool
, build :
∀(a : Type)
→ ( ∀(optional : Type)
→ ∀(just : a → optional)
→ ∀(nothing : optional)
→ optional
)
→ Optional a
, concat :
∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a
, filter :
∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a
, fold :
∀(a : Type)
→ Optional a
→ ∀(optional : Type)
→ ∀(just : a → optional)
→ ∀(nothing : optional)
→ optional
, head :
∀(a : Type) → ∀(xs : List (Optional a)) → Optional a
, last :
∀(a : Type) → ∀(xs : List (Optional a)) → Optional a
, length :
∀(a : Type) → ∀(xs : Optional a) → Natural
, map :
∀(a : Type)
→ ∀(b : Type)
→ ∀(f : a → b)
→ ∀(o : Optional a)
→ Optional b
, null :
∀(a : Type) → ∀(xs : Optional a) → Bool
, toList :
∀(a : Type) → ∀(o : Optional a) → List a
, unzip :
∀(a : Type)
→ ∀(b : Type)
→ ∀(xs : Optional { _1 : a, _2 : b })
→ { _1 : Optional a, _2 : Optional b }
}
, Text :
{ concat :
∀(xs : List Text) → Text
, concatMap :
∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text
, concatMapSep :
∀(separator : Text)
→ ∀(a : Type)
→ ∀(f : a → Text)
→ ∀(elements : List a)
→ Text
, concatSep :
∀(separator : Text) → ∀(elements : List Text) → Text
, show :
Text → Text
}
, XML :
{ attribute :
∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }
, element :
∀ ( elem
: { attributes :
List { mapKey : Text, mapValue : Text }
, content :
List
( ∀(XML : Type)
→ ∀ ( xml
: { element :
{ attributes :
List { mapKey : Text, mapValue : Text }
, content :
List XML
, name :
Text
}
→ XML
, text :
Text → XML
}
)
→ XML
)
, name :
Text
}
)
→ ∀(XML : Type)
→ ∀ ( xml
: { element :
{ attributes :
List { mapKey : Text, mapValue : Text }
, content :
List XML
, name :
Text
}
→ XML
, text :
Text → XML
}
)
→ XML
, emptyAttributes :
List { mapKey : Text, mapValue : Text }
, leaf :
∀ ( elem
: { attributes :
List { mapKey : Text, mapValue : Text }
, name :
Text
}
)
→ ∀(XML : Type)
→ ∀ ( xml
: { element :
{ attributes :
List { mapKey : Text, mapValue : Text }
, content :
List XML
, name :
Text
}
→ XML
, text :
Text → XML
}
)
→ XML
, render :
∀ ( x
: ∀(XML : Type)
→ ∀ ( xml
: { element :
{ attributes :
List { mapKey : Text, mapValue : Text }
, content :
List XML
, name :
Text
}
→ XML
, text :
Text → XML
}
)
→ XML
)
→ Text
, text :
∀(d : Text)
→ ∀(XML : Type)
→ ∀ ( xml
: { element :
{ attributes :
List { mapKey : Text, mapValue : Text }
, content :
List XML
, name :
Text
}
→ XML
, text :
Text → XML
}
)
→ XML
}
}