/dada/Natural/lt

Copy path to clipboard

Source

let P =
https://prelude.dhall-lang.org/v20.1.0/package.dhall sha256:26b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98

let Natural/recursive = ./recursive

let Natural/steppable = ./steppable

in λ(a : Natural) →
λ(b : Natural) →
P.Optional.fold
Natural
( Natural/recursive.cata
(Optional Natural)
( λ(x : Optional (Optional Natural)) →
P.Optional.fold
(Optional Natural)
x
(Optional Natural)
( λ(y : Optional Natural) →
P.Optional.fold
Natural
y
(Optional Natural)
Natural/steppable.project
(None Natural)
)
(Natural/steppable.project b)
)
a
)
Bool
(λ(_ : Natural) → True)
False