File: notations.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (43 lines) | stat: -rw-r--r-- 925 bytes parent folder | download | duplicates (4)
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
43
From Ltac2 Require Import Ltac2.
From Coq Require Import ZArith String List.

(** * Test cases for the notation system itself *)

Open Scope Z_scope.

Check 1 + 1 : Z.

Ltac2 Notation "ex" arg(constr(nat,Z)) := arg.

Check (1 + 1)%nat%Z = 1%nat.

Lemma two : nat.
  refine (ex (1 + 1)).
Qed.

Import ListNotations.
Close Scope list_scope.

Ltac2 Notation "sl" arg(constr(string,list)) := arg.

Lemma maybe : list bool.
Proof.
  refine (sl ["left" =? "right"]).
Qed.

Lemma Z_add_bounds {amin a amax bmin b bmax : Z}:
  amin <= a <= amax ->
  bmin <= b <= bmax ->
  amin + bmin <= a + b <= amax + bmax.
Admitted.

Lemma apply l1 l2 v1 v2 u1 u2 : l1 + l2 <= v1 + v2 <= u1 + u2.
Proof.
  apply Z_add_bounds.
Admitted.

(** * Test cases for specific notations with special contexts *)

(** ** Test eval ... in / reduction tactics *)

(** Moved to test-suite/output/ltac2_notations_eval_in.v so that the output can be checked s*)