Currently there is no way of defining functions erasable functions, this is a main issue as functions such as identity require those (A : Type $ 0) => (x : A $ 1) => x.
This PR introduces it in a very limited way, allowing only erasable and non erasable functions.
Goals
Unlock erasable parametric functions.
Context
Currently there is no way of defining functions erasable functions, this is a main issue as functions such as identity require those
(A : Type $ 0) => (x : A $ 1) => x.This PR introduces it in a very limited way, allowing only erasable and non erasable functions.