Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon".
(* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
-Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
-Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
-Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
-Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
-Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
+Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
+Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
+Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
+Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
+Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
-Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
-Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
-Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
- Extraction Inline CoreIPName.
+Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
+Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
+Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
+ Extraction Inline CoreIPName.
(* This type extracts exactly onto GHC's Literal.Literal type *)
Inductive HaskLiteral :=
Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable PairTyCon : TyFun. Extract Inlined Constant PairTyCon => "TysWiredIn.pairTyCon".
+Variable UnitTyCon : TyFun. Extract Inlined Constant UnitTyCon => "TysWiredIn.unitTyCon".
Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".