GitLab

confluence and prohibited applications of rewrite rules

Otherwise the system is not confluent since char is not in normal form.

I don't think that proof irrelevance is the good way to go.

Two levels of partial functions : partial typing functions and partially typed partial functions.

Still unfinished.

Theory looks quite OK but not yet usable.
It is harder than expected to prove that when f is defined on D then f[l<-A] is defined on (cons l D).

Partial functions are allowed to be defined outside the domain they will be called on.

Work in progress, these files don't typecheck yet.