TODO: keep track of match branching
This commit is contained in:
parent
66226ac725
commit
b6c934b9f3
|
@ -158,6 +158,7 @@
|
||||||
[⊢ (match- e- [p- s-] ...
|
[⊢ (match- e- [p- s-] ...
|
||||||
[_ (#%app- error- "incomplete pattern match")])
|
[_ (#%app- error- "incomplete pattern match")])
|
||||||
(⇒ : (U τ-s ...))
|
(⇒ : (U τ-s ...))
|
||||||
|
;; TODO losing branching information here
|
||||||
(⇒ ν-ep (eps ... ...))
|
(⇒ ν-ep (eps ... ...))
|
||||||
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
||||||
(⇒ ν-s (ss ... ...))])
|
(⇒ ν-s (ss ... ...))])
|
||||||
|
|
Loading…
Reference in New Issue