mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Create reflexivity.kind
This commit is contained in:
parent
1a2ef75255
commit
7218d9f2e0
8
base/Nat/Order/reflexivity.kind
Normal file
8
base/Nat/Order/reflexivity.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.Order.refl(a: Nat): Equal<Bool>(Nat.lte(a, a), true)
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Bool>(true)
|
||||
succ:
|
||||
let ind = Nat.Order.refl(a.pred)
|
||||
ind
|
||||
}: Equal<Bool>(Nat.lte(a, a), true)
|
Loading…
Reference in New Issue
Block a user