diff options
| author | Maxime Dénès | 2014-06-02 14:47:09 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 18:05:01 -0400 |
| commit | b5ed7e2a5700da0ee7930069c0e58c35f2af410c (patch) | |
| tree | 08ff321f60d3984cb671800a1cfd0fe7d497571c /checker/type_errors.ml | |
| parent | 0ebd3def1fe2bae9c545e8244028197a589cf4db (diff) | |
Extend subterm relation to pattern matching in return predicates.
A pattern matching is can now be a subterm if:
- Every branch is a subterm
- The return predicate is a pattern matching whose return predicate is an arity.
- That pattern matching (in the return predicate) returns the same inductive
family in the conclusion of each branch.
The commutative cut rule hasn't been updated accordingly yet.
Diffstat (limited to 'checker/type_errors.ml')
0 files changed, 0 insertions, 0 deletions