Improve Pruviloj.Induction.induction error message
The current error message is a bit cryptic.
Replace it with @david-christiansen's suggestion.
See discussion on #3594 for details.
Close #3594
commit22bd91a4b4a5cebd12985e95222e1c90c2f09744
authorEric Bailey <eric@ericb.me>
dateWed 28 Dec 2016, 18:50 (10 years ago)
parent24c796a
libs/pruviloj/Pruviloj/Induction.idr+3−1
@@ -132,7 +132,9 @@ induction subj =
132132 (_, ty) <- check !getEnv subj
133133 ty' <- forget ty
134134 case headName ty' of
135− Nothing => fail [TermPart ty, TextPart "is not an inductive family"]
135+ Nothing =>
136+ fail [TermPart ty,
137+ TextPart "is not a datatype declared with the data keyword"]
136138 Just fam =>
137139 do let elim = elimN fam
138140 (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim