@@ -69,11 +69,10 @@ record TyDecl where
69 returnType : Raw
69 returnType : Raw
72−-- Note: FunClause is not a record because impossible clauses may be
73−-- added at some point.
74||| A single pattern-matching clause
72||| A single pattern-matching clause
75data FunClause : Type where
73data FunClause : Type where
76 MkFunClause : (lhs, rhs : Raw) -> FunClause
74 MkFunClause : (lhs, rhs : Raw) -> FunClause
75+ MkImpossibleClause : (lhs : Raw) -> FunClause
78||| A reflected function definition.
77||| A reflected function definition.
79record FunDefn where
78record FunDefn where