functiontypesnumbersidrisproof-of-correctness

Idris, typed addition (incrementation)

How can I write function like this

data Wrap : Nat -> Type where
  Wrp : n -> Wrap n

addOne : (n : Nat) -> Wrap (S n)
addOne {n} = Wrp (S n)

in a form like this

addOne : (n : Nat) -> S n
addOne {n} = S n

or something similar?

Thanks

Solution

  • addOne : (n : Nat) -> S n wouldn't be valid, as the return type wouldn't be a type, but a value. Closest thing to what you might want would be

    addOne : (n : Nat) -> (k : Nat ** k = S n)
addOne n = (S n ** Refl)

    where addOne would return a tuple of some Nat and a proof, that this Nat is indeed S n. Or proving that property afterwards:

    addOne : (n : Nat) -> Nat
addOne n = S n

addOneIsSucc : (n : Nat) -> addOne n = S n
addOneIsSucc n = Refl