a function can be passed a postulate as an irrelevant argument and still still compute a result

Irrelevance.agda

-- a demonstration that a function can be passed a postulate as an irrelevant
-- argument and still still compute a result
module Irrelevance where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning


postulate
  undefined : ℕ

data Vec (A : Set) : ℕ → Set where
  nil
    : Vec A 0
  cons
    : {n : ℕ}
    → A
    → Vec A n
    → Vec A (suc n)

length : {A : Set} → {n : ℕ} → Vec A n → ℕ
length nil
  = 0
length (cons _ xs)
  = 1 + length xs

test : length {ℕ} {undefined} (cons 1 (cons 2 nil)) ≡ 2
test = refl