idris-0.9.13: test/totality007/src/Totality.idr

module Totality

total foo : Nat -> Nat
foo Z = Z