{-# LANGUAGE ExistentialQuantification, GADTs #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Type
( Type (..)
, U (..)
, U2 (..)
) where
import Copilot.Core.Type.Equality
data Type a where
Bool :: Type Bool
Integer :: Type Integer
Real :: Type Double
instance EqualType Type where
Bool =~= Bool = Just Refl
Integer =~= Integer = Just Refl
Real =~= Real = Just Refl
_ =~= _ = Nothing
data U f = forall t . U (f t)
data U2 f g = forall t . U2 (f t) (g t)
instance Show (Type t) where
show Integer = "Int"
show Bool = "Bool"
show Real = "Real"