36 lines
765 B
Coq
36 lines
765 B
Coq
Require Import List.
|
|
Import ListNotations.
|
|
|
|
Section Foo.
|
|
Context {A:Type}.
|
|
|
|
Definition hdpf (l:list A) (pf: l <> []): A :=
|
|
(match l return l <> [] -> A with
|
|
| [] => fun pf' => match pf' eq_refl with end
|
|
| x::_ => fun _ => x
|
|
end) pf.
|
|
End Foo.
|
|
|
|
Ltac tacNotNil l := unfold l; intros H; inversion H.
|
|
|
|
Example l1 := [1;2;3].
|
|
|
|
Lemma l1NotNil: l1 <> [].
|
|
Proof. tacNotNil l1. Qed.
|
|
|
|
Compute hdpf [1;2;3] (ltac:(tacNotNil l1)).
|
|
(* = 1 : nat *)
|
|
|
|
Compute
|
|
let l := [1] in
|
|
hdpf l (ltac:(tacNotNil l)).
|
|
|
|
Compute
|
|
let l := [true; false] in
|
|
hdpf l (ltac:(tacNotNil l)).
|
|
|
|
Compute
|
|
let l := [] in
|
|
hdpf l (ltac:(tacNotNil l)).
|
|
(* I wonder why this didn't give an outright error... *)
|