blob: 4a11e7cae05a132ebbe39a8332ef56785ef1cdb6 (
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
39
40
41
42
|
From Ltac2 Require Import Ltac2.
From Coq Require Import ZArith.
(** * Test eval ... in / reduction tactics *)
(** The below test cases test if the notation syntax works - not the tactics as such *)
Ltac2 Eval (eval red in (1+2+3)).
Ltac2 Eval (eval hnf in (1+2+3)).
Ltac2 Eval (eval simpl in (1+2+3)).
Ltac2 Eval (eval simpl Z.add in (1+2+3)).
Ltac2 Eval (eval cbv in (1+2+3)).
Ltac2 Eval (eval cbv delta [Z.add] beta iota in (1+2+3)).
Ltac2 Eval (eval cbv delta [Z.add Pos.add] beta iota in (1+2+3)).
Ltac2 Eval (eval cbn in (1+2+3)).
Ltac2 Eval (eval cbn delta [Z.add] beta iota in (1+2+3)).
Ltac2 Eval (eval cbn delta [Z.add Pos.add] beta iota in (1+2+3)).
Ltac2 Eval (eval lazy in (1+2+3)).
Ltac2 Eval (eval lazy delta [Z.add] beta iota in (1+2+3)).
Ltac2 Eval (eval lazy delta [Z.add Pos.add] beta iota in (1+2+3)).
(* The example for [fold] in the reference manual *)
Ltac2 Eval (
let t1 := '(~0=0) in
let t2 := eval unfold not in $t1 in
let t3 := eval pattern (0=0) in $t2 in
let t4 := eval fold not in $t3 in
[t1; t2; t3; t4]
).
|
