Add MkImpossibleClause constructor to FunClause
This isn't useful for defineFunction yet, because the reflection impl
tries to typecheck the LHS. That should be fixed at some point, but
this will be useful for function definition lookup as well.
commita7754a028e2e7785ae010234f7ddd4eb6eb45647
authorShea Levy <shea@shealevy.com>
dateWed 11 Nov 2015, 18:46 (11 years ago)
parentb49893e
libs/prelude/Language/Reflection/Elab.idr+1−2
@@ -69,11 +69,10 @@ record TyDecl where
6969 returnType : Raw
7070
7171
72−-- Note: FunClause is not a record because impossible clauses may be
73−-- added at some point.
7472||| A single pattern-matching clause
7573data FunClause : Type where
7674 MkFunClause : (lhs, rhs : Raw) -> FunClause
75+ MkImpossibleClause : (lhs : Raw) -> FunClause
7776
7877||| A reflected function definition.
7978record FunDefn where