1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* Weird corner case accepted by the pattern-matching algorithm. Destructuring
let-bindings in patterns can actually be shorter than the case they match. *)
Inductive ascii : Set :=
| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii.
Definition dummy (a : ascii) : unit :=
let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt.
Goal forall (a : ascii) (H : tt = dummy a), True.
Proof.
intros a H.
unfold dummy in *.
(* Two bound variables in the pattern, eight in the term. *)
match goal with
| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:?
end.
Abort.
|
