@@ -54,25 +54,28 @@ data TyConArg =
54 TyConIndex FunArg
54 TyConIndex FunArg
56||| A type declaration
56||| A type declaration
57−data TyDecl : Type where
57+record TyDecl where
58− ||| A type declaration.
58+ constructor Declare
60− ||| Each argument is in the scope of the names of previous
60+ ||| The name of the function being declared.
61− ||| arguments, and the return type is in the scope of all the
61+ tyDeclName : TTName
62− ||| argument names.
62+
63− |||
63+ ||| Each argument is in the scope of the names of previous arguments.
64− ||| @ fn the name to be declared, fully-qualified
64+ tyDeclArgs : List FunArg
65− ||| @ args the arguments to the function
65+
66− ||| @ ret the final return type
66+ ||| The return type is in the scope of all the argument names.
67− Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl
67+ tyDeclReturnTy : Raw
69||| A single pattern-matching clause
70||| A single pattern-matching clause
70data FunClause : Type where
71data FunClause : Type where
71 MkFunClause : (lhs, rhs : Raw) -> FunClause
72 MkFunClause : (lhs, rhs : Raw) -> FunClause
73||| A reflected function definition.
74||| A reflected function definition.
74−data FunDefn : Type where
75+record FunDefn where
76+ constructor DefineFun
75− DefineFun : TTName -> List FunClause -> FunDefn
78+ funDefnClauses : List FunClause
78data CtorArg = CtorParameter FunArg | CtorField FunArg
81data CtorArg = CtorParameter FunArg | CtorField FunArg