-
Notifications
You must be signed in to change notification settings - Fork 24
/
Member.lean
47 lines (37 loc) · 1.14 KB
/
Member.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
/-
Copyright (c) 2021-2024 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.Rule
namespace Aesop
inductive BaseRuleSetMember
| normRule (r : NormRule)
| unsafeRule (r : UnsafeRule)
| safeRule (r : SafeRule)
| unfoldRule (r : UnfoldRule)
deriving Inhabited
def BaseRuleSetMember.name : BaseRuleSetMember → RuleName
| normRule r => r.name
| unsafeRule r => r.name
| safeRule r => r.name
| unfoldRule r => r.name
inductive GlobalRuleSetMember
| base (m : BaseRuleSetMember)
| normSimpRule (e : NormSimpRule)
deriving Inhabited
def GlobalRuleSetMember.name : GlobalRuleSetMember → RuleName
| base m => m.name
| normSimpRule r => r.name
inductive LocalRuleSetMember
| global (m : GlobalRuleSetMember)
| localNormSimpRule (r : LocalNormSimpRule)
deriving Inhabited
def LocalRuleSetMember.name : LocalRuleSetMember → RuleName
| global m => m.name
| localNormSimpRule r => r.name
def LocalRuleSetMember.toGlobalRuleSetMember? :
LocalRuleSetMember → Option GlobalRuleSetMember
| global m => some m
| _ => none
end Aesop