Counter with upper limit in Idris

Question

I am reading "Type-driven development with Idris" now so I created one rather artificial example as an experiment. It's a counter which fails to type-check when trying to decrease a zero value.

Here is the code:

data Counter : Nat -> Type where
  Value : (n : Nat) -> Counter n

data CounterOp : Type -> (before : Nat) -> (after : Nat) -> Type where
     Incr     : CounterOp () value (S value)
     Decr     : CounterOp () (S value) value
     GetValue : CounterOp Nat value value

     Pure : ty -> CounterOp ty value value
     (>>=) : CounterOp a value1 value2 ->
             (a -> CounterOp b value2 value3) ->
             CounterOp b value1 value3

runCounterOp : (val : Counter inValue) ->
           CounterOp ty inValue outValue ->
           (ty, Counter outValue)
runCounterOp (Value value) Incr = ((), Value (S value))
runCounterOp (Value (S value)) Decr = ((), Value value)
runCounterOp (Value value) GetValue = (value, Value value)
runCounterOp value (Pure x) = (x, value)
runCounterOp value (x >>= f) =
  let (x', value') = runCounterOp value x in
  runCounterOp value' (f x')

So it is impossible to run runCounterOp (Value 0) Decr.

Now I want to change it so it fails to type-check when it's more than 10 (so run runCounterOp (Value 10) Incr is impossible) but I don't know how. As I understand I should use LTE somehow but don't understand how.

Any ideas?

Answer 1

You can either change Nat for Fin 10 or add to Incr a parameter (either explicit or automatically resolved) that contains the proof that the initial value is below 10: Incr : {auto prf : LT value 10} -> CounterOp () value (S value).