@@ -54,25 +54,28 @@ data TyConArg =
5454 TyConIndex FunArg
5555
5656||| A type declaration
57−data TyDecl : Type where
58− ||| A type declaration.
59− |||
60− ||| Each argument is in the scope of the names of previous
61− ||| arguments, and the return type is in the scope of all the
62− ||| argument names.
63− |||
64− ||| @ fn the name to be declared, fully-qualified
65− ||| @ args the arguments to the function
66− ||| @ ret the final return type
67− Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl
57+record TyDecl where
58+ constructor Declare
59+
60+ ||| The name of the function being declared.
61+ tyDeclName : TTName
62+
63+ ||| Each argument is in the scope of the names of previous arguments.
64+ tyDeclArgs : List FunArg
65+
66+ ||| The return type is in the scope of all the argument names.
67+ tyDeclReturnTy : Raw
68+
6869
6970||| A single pattern-matching clause
7071data FunClause : Type where
7172 MkFunClause : (lhs, rhs : Raw) -> FunClause
7273
7374||| A reflected function definition.
74−data FunDefn : Type where
75− DefineFun : TTName -> List FunClause -> FunDefn
75+record FunDefn where
76+ constructor DefineFun
77+ funDefnName : TTName
78+ funDefnClauses : List FunClause
7679
7780
7881data CtorArg = CtorParameter FunArg | CtorField FunArg