[ libs ] add DecEq to Prelude

This commit is contained in:
2025-07-27 14:57:21 -07:00
parent bcf34c0941
commit 0c72d690e3
3 changed files with 11 additions and 18 deletions

View File

@@ -6,22 +6,6 @@ module RunLength
import Prelude
-- TODO this belongs in a library
data Void : U where
Not : U U
Not x = x Void
data Dec : U U where
Yes : prop. (prf : prop) Dec prop
No : prop. (contra : Not prop) Dec prop
class DecEq t where
decEq : (x₁ : t) (x₂ : t) Dec (x₁ x₂)
-- end lib
rep : a. Nat a List a
rep Z x = Nil
rep (S k) x = x :: rep k x