Experiments with refutation and paraconsistency.
Contains a port of Allais, "Typing with Leftovers: A mechanization of Intuitionistic Multiplicative-Additive Linear Logic".
Requires Idris 2.
Experiments with refutation and paraconsistency.
Contains a port of Allais, "Typing with Leftovers: A mechanization of Intuitionistic Multiplicative-Additive Linear Logic".
Requires Idris 2.