Linearity is exclusive to Idris 2, compile time only values/run-time erasure are supported by all major proof assistants. Coq and Lean have the Prop type (compi

Linearity is exclusive to Idris 2, compile time only values/run-time erasure are supported by all major proof assistants. Coq and Lean have the Prop type (compile time only) while Agda allows annotation of variables as run-time irrelevant.