{-# 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
Type a
Bool =~= :: Type a -> Type b -> Maybe (Equal a b)
=~= Type b
Bool = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
Type a
Integer =~= Type b
Integer = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
Type a
Real =~= Type b
Real = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
Type a
_ =~= Type b
_ = Maybe (Equal a b)
forall a. Maybe a
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 :: Type t -> String
show Type t
Integer = String
"Int"
show Type t
Bool = String
"Bool"
show Type t
Real = String
"Real"