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
39
40
41
|
Require Import Ltac2.Ltac2.
Ltac2 Type exn ::= [ Regression_Test_Failure ].
Ltac2 check_eq_int_array(a1: int array)(a2: int array) :=
if Array.equal Int.equal a1 a2 then () else Control.throw Regression_Test_Failure.
Goal True.
check_eq_int_array [| 1; 22; 333 |] (Array.of_list [1; 22; 333]).
check_eq_int_array [| 22 |] (Array.of_list [22]).
check_eq_int_array [| |] (Array.of_list []). (* space between [| and |] is mandatory *)
constructor.
Qed.
(* Test that tactic dispatch where "[|" is two tokens still works: *)
Goal True /\ True.
Proof.
split > [|constructor]. constructor.
Qed.
Goal forall a b: nat, a = b -> True /\ a = b /\ True.
Proof.
intros.
(split > [|split]) > [|exact H|].
all: constructor.
Qed.
Set Default Proof Mode "Classic".
Goal True /\ True.
Proof.
split; [|constructor]. constructor.
Qed.
Goal forall a b: nat, a = b -> True /\ a = b /\ True.
Proof.
intros.
(split; [|split]); [|exact H|].
all: constructor.
Qed.
|
