mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-07-14 22:50:28 +03:00
19 lines
226 B
Plaintext
19 lines
226 B
Plaintext
use Nat/{succ,zero}
|
|
use Bool/{true,false}
|
|
|
|
is_ltn
|
|
- a: Nat
|
|
- b: Nat
|
|
: Bool
|
|
|
|
match a with (b: Nat) {
|
|
zero: match b {
|
|
zero: false
|
|
succ: true
|
|
}
|
|
succ: match b {
|
|
zero: false
|
|
succ: (is_ltn a.pred b.pred)
|
|
}
|
|
}
|