summaryrefslogtreecommitdiff
path: root/src/Data/These/Decidable.idr
AgeCommit message (Collapse)Author
2024-10-28Make everything relevant.Greg Brown
Too few proofs were relevant. Now they are.
2024-09-09Restart.Greg Brown
- use De Bruijn, as Namely, Painless had more pain than promised; - remove higher-kinded types; - provide ill-typing predicates; - prove substitution respects ill-typing;