agda question prove Prove fact0factorial Forall n N rightarr

agda question

prove

Prove fact0-factorial: Forall (n: N) rightarrow fact n 0 factorial n fact0-factorial = {} 0

Solution

module factorial where

open import type

open import Data.zero

open import Data.Nat

data Fact :N -> N set where

fact : N -> N

fact 0 = 1

fact (suc n) = (suc n) * (fact n)

getFact : n -> Fact n (fact n)

getFact 0 = factzero

getFact (suc n) = factsuc (getFact n)