fix: handle the TermEx->OptTermEx injection in Statix

This commit is contained in:
Glen Whitney 2021-02-17 19:47:29 -08:00
parent f93499acfd
commit 2514f0df98

View File

@ -140,10 +140,15 @@ hand-defined, as done in "statics/util.stx" like so:
@l.type := T. @l.type := T.
type_Ex : Ex -> TYPE type_Ex : Ex -> TYPE
type_TermEx : TermEx -> TYPE
type_OptTermEx(ote@Ex2OptTermEx(e)) = T :- type_OptTermEx(ote@Ex2OptTermEx(e)) = T :-
type_Ex(e) == T, type_Ex(e) == T,
@ote.type :=T. @ote.type := T.
type_OptTermEx(ote@TermEx2OptTermEx(te)) = T :-
type_TermEx(te) == T,
@ote.type := T.
/** md /** md
@ -171,8 +176,6 @@ constructor was trivial:
``` ```
**/ **/
type_TermEx: TermEx -> TYPE
type_TermEx(te@Terminate(e)) = T :- type_TermEx(te@Terminate(e)) = T :-
type_Ex(e) == T, type_Ex(e) == T,
@te.type := T. @te.type := T.