gistfile1.idr

data type : Type where
  nat : type
  bool : type

data tbinop : type -> type -> type -> Type where
  TPlus : tbinop nat nat nat
  TTimes : tbinop nat nat nat
  TEq : (t : type) -> tbinop t t bool
  TLt : tbinop nat nat bool

data texp : type -> Type where
  TNConst : Nat -> texp nat
  TBConst : Bool -> texp bool
  TBinop : tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t

typeDenote : type -> Type
typeDenote nat = Nat
typeDenote bool = Bool

tbinopDenote : tbinop arg1 arg2 res ->
               typeDenote arg1 -> typeDenote arg2 -> typeDenote res
tbinopDenote TPlus = plus
tbinopDenote TTimes = mult
tbinopDenote (TEq nat) = (==)
tbinopDenote (TEq bool) = (==)
tbinopDenote TLt = (<)

-- line 24 col 14
--      Can't convert
--              tbinop nat nat bool
--      with
--              tbinop nat arg2 bool