blob: cfef2e37bea5427ecf7027c3851be3057af035b6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
Require Import ssreflect.
Ltac fancy := case; last first.
Notation fancy := (ltac:( fancy )).
Ltac replicate n :=
let what := fresh "_replicate_" in
move=> what; do n! [ have := what ]; clear what.
Notation replicate n := (ltac:( replicate n )).
Lemma foo x (w : nat) (J : bool -> nat -> nat) : exists y, x=0+y.
Proof.
move: (w) => /ltac:(idtac) _.
move: w => /(replicate 6) w1 w2 w3 w4 w5 w6.
move: w1 => /J/fancy [w'||];last exact: false.
move: w' => /J/fancy[w''||]; last exact: false.
by exists x.
by exists x.
by exists x.
Qed.
Ltac unfld what := rewrite /what.
Notation "% n" := (ltac:( unfld n )) (at level 0) : ssripat_scope.
Notation "% n" := n : nat_scope.
Open Scope nat_scope.
Definition def := 4.
Lemma test : True -> def = 4.
Proof.
move=> _ /(% def).
match goal with |- 4 = 4 => reflexivity end.
Qed.
|
