gistfile1.idr

-- - + Errors (2)
--  |-- (eliminator) line 0 col 0:
--  |   Can't convert
--  |           texp t__4
--  |   with
--  |           texp t
--  `--  line 0 col 0:
--      No type declaration for <<Main.texp eliminator>>

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

%elim
data texp : type -> Type where
  TNConst : Nat -> texp nat
  TBConst : Bool -> texp bool
  TBinop : (t1, t2, t : type) -> tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t