0 | module Data.Fuel
 1 |
 2 | %default total
 3 |
 4 | ||| Fuel for running total operations potentially indefinitely.
 5 | public export
 6 | data Fuel = Dry | More (Lazy Fuel)
 7 |
 8 | ||| Provide `n` units of fuel.
 9 | public export
10 | limit : Nat -> Fuel
11 | limit  Z    = Dry
12 | limit (S n) = More (limit n)
13 |
14 | ||| Provide fuel indefinitely.
15 | ||| This function is fundamentally partial.
16 | export
17 | covering
18 | forever : Fuel
19 | forever = More forever
20 |