blob: 3207e5983fd243fe6b14e04ea9f9fc55f5bbfc1a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Import String.
Record test := { field : nat }.
Open Scope string_scope.
Unset Printing Notations.
Check "foo".
Check 1234.
Check 1 + 2.
Check match "a" with "a" => true | _ => false end.
Check match 1 with 1 => true | _ => false end.
Check {| field := 7 |}.
Set Printing Raw Literals.
Check "foo".
Check 1234.
Check 1 + 2.
Check match "a" with "a" => true | _ => false end.
Check match 1 with 1 => true | _ => false end.
Check {| field := 7 |}.
|
