Coq Extended Pattern Match - Program Definition

Program.v

Require Import Program.Tactics.

Lemma prf (n : nat)(p : n = 0) : bool.
Admitted.

Program Definition huh(n : nat) : bool :=
  match n with
  | O => prf n _.   (* Program adds the equation `n = 0` to the context of this match branch which is pickec up by the implicit *) 
  | S n => true
end.

(* 
Agda does not have this?
prf : ∀{n : ℕ} → (p : n ≡ 0) → Bool  
prf = {!   !}

huh : ℕ → Bool 
huh n@zero = prf {n} _
huh _ = true

*)

https://coq.inria.fr/refman/addendum/program.html

See "Generation of Equalities"

match x with
| 0 => t
| S n => u
end.

rewritten to

(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
end) (eq_refl x).