1 (*********************************************************************************************************************************)
2 (* HaskCoreVars: basically GHC's Var.Var imported into Coqland *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
10 (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *)
11 Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var".
12 Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)".
13 Variable coreVarToString : CoreVar -> string. Extract Inlined Constant coreVarToString => "outputableToString".
14 Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }.
15 Instance CoreVarToString : ToString CoreVar :=
16 { toString := coreVarToString }.