-
Notifications
You must be signed in to change notification settings - Fork 30
/
Copy pathAddRulesCommand.lean
94 lines (62 loc) · 1.38 KB
/
AddRulesCommand.lean
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
/-
Copyright (c) 2024 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop
set_option aesop.check.all true
set_option aesop.smallErrorMessages true
-- Basic examples
structure TT₁ where
/-- error: tactic 'aesop' failed, made no progress -/
#guard_msgs in
example : TT₁ := by
aesop
add_aesop_rules safe TT₁
example : TT₁ := by
aesop
-- Local rules
structure TT₂ where
namespace Test
local add_aesop_rules safe TT₂
example : TT₂ := by
aesop
end Test
/-- error: tactic 'aesop' failed, made no progress -/
#guard_msgs in
example : TT₂ := by
aesop
-- Scoped rules
structure TT₃ where
namespace Test
scoped add_aesop_rules safe TT₃
example : TT₃ := by
aesop
end Test
/-- error: tactic 'aesop' failed, made no progress -/
#guard_msgs in
example : TT₃ := by
aesop
def Test.example : TT₃ := by
aesop
-- Tactics
structure TT₄ where
/-- error: tactic 'aesop' failed, made no progress -/
#guard_msgs in
example : TT₄ := by
aesop
add_aesop_rules safe (by exact TT₄.mk)
example : TT₄ := by
aesop
-- Multiple rules
axiom T : Type
axiom U : Type
axiom f : T → U
axiom t : T
/-- error: tactic 'aesop' failed, made no progress -/
#guard_msgs in
example : U := by
aesop
add_aesop_rules safe [(by apply f), t]
noncomputable example : U := by
aesop