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
|
Section S.
Variables (a:nat) (b:bool).
Fail Set Default Proof Using ")".
Fail Set Default Proof Using "a)".
Fail Set Default Proof Using "(a . )".
Fail Set Default Proof Using "(a .".
Set Default Proof Using "".
Lemma foo1 : True.
Proof. trivial. Qed.
Set Default Proof Using "()".
Lemma foo2 : True.
Proof. trivial. Qed.
Set Default Proof Using "( )".
Lemma foo2' : True.
Proof. trivial. Qed.
Set Default Proof Using "a b".
Lemma foo3 : True.
Proof. trivial. Qed.
Set Default Proof Using "(b a)".
Lemma foo4 : True.
Proof. trivial. Qed.
End S.
Check foo1 : True.
Check foo2 : True.
Check foo2' : True.
Check foo3 : nat -> bool -> True.
Check foo4 : nat -> bool -> True.
Require Import Coq.ssr.ssreflect.
(* ssr makes "\*\)" parse differently so preprocessing has to make sure to insert a space *)
Set Default Proof Using "Type*".
|
