@@ -132,7 +132,9 @@ induction subj =
132 (_, ty) <- check !getEnv subj
132 (_, ty) <- check !getEnv subj
133 ty' <- forget ty
133 ty' <- forget ty
134 case headName ty' of
134 case headName ty' of
135− Nothing => fail [TermPart ty, TextPart "is not an inductive family"]
136+ fail [TermPart ty,
137+ TextPart "is not a datatype declared with the data keyword"]
136 Just fam =>
138 Just fam =>
137 do let elim = elimN fam
139 do let elim = elimN fam
138 (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim
140 (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim