X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskCoreVars.v;h=9225974e0dc3e7a2a6db4a52c432495f64ccca9d;hb=8efffc7368b5e54c42461f45a9708ff2828409a4;hp=a55c09b187a9aceaa75451bd66f5bb9660b8c6bf;hpb=5a0761840d89b82cdacb0bf9215fd41aba847b68;p=coq-hetmet.git diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index a55c09b..9225974 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -5,14 +5,12 @@ Generalizable All Variables. Require Import Preamble. Require Import General. -Require Import HaskGeneral. +Require Import Coq.Strings.String. (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *) Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var". Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)". -Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). -Instance CoreVarEqDecidable : EqDecidable CoreVar := -{ eqd_dec := coreVar_eq -(*; eqd_dec_reflexive := coreVar_eq_refl*) -}. - +Variable coreVarToString : CoreVar -> string. Extract Inlined Constant coreVarToString => "outputableToString". +Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }. +Instance CoreVarToString : ToString CoreVar := + { toString := coreVarToString }.