-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathInterpretabilityLogicArchive.lean
More file actions
68 lines (67 loc) · 4.1 KB
/
Copy pathInterpretabilityLogicArchive.lean
File metadata and controls
68 lines (67 loc) · 4.1 KB
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
module -- shake: keep-all --deprecated_module: ignore
public import InterpretabilityLogicArchive.Axioms
public import InterpretabilityLogicArchive.Entailment
public import InterpretabilityLogicArchive.Entailment.Basic
public import InterpretabilityLogicArchive.Entailment.CL
public import InterpretabilityLogicArchive.Entailment.IL
public import InterpretabilityLogicArchive.Entailment.ILMinus
public import InterpretabilityLogicArchive.Entailment.ILMinus_J1
public import InterpretabilityLogicArchive.Entailment.ILMinus_J2
public import InterpretabilityLogicArchive.Entailment.ILMinus_J4
public import InterpretabilityLogicArchive.Entailment.ILMinus_J5
public import InterpretabilityLogicArchive.Entailment.ILMinus_M
public import InterpretabilityLogicArchive.Entailment.IL_KW1Zero
public import InterpretabilityLogicArchive.Entailment.IL_KW2
public import InterpretabilityLogicArchive.Entailment.IL_M
public import InterpretabilityLogicArchive.Entailment.IL_M₀
public import InterpretabilityLogicArchive.Entailment.IL_M₀_W
public import InterpretabilityLogicArchive.Entailment.IL_P
public import InterpretabilityLogicArchive.Entailment.IL_R
public import InterpretabilityLogicArchive.Entailment.IL_R_W
public import InterpretabilityLogicArchive.Entailment.IL_Rstar
public import InterpretabilityLogicArchive.Entailment.IL_W
public import InterpretabilityLogicArchive.Entailment.IL_Wstar
public import InterpretabilityLogicArchive.Formula.Basic
public import InterpretabilityLogicArchive.Formula.OfModal
public import InterpretabilityLogicArchive.Formula.Substitution
public import InterpretabilityLogicArchive.Formula.ToModal
public import InterpretabilityLogicArchive.Hilbert.Axiom
public import InterpretabilityLogicArchive.Hilbert.Basic.Basic
public import InterpretabilityLogicArchive.Hilbert.Basic_Minimal
public import InterpretabilityLogicArchive.Hilbert.Minimal.Basic
public import InterpretabilityLogicArchive.Logic.Basic
public import InterpretabilityLogicArchive.LogicSymbol
public import InterpretabilityLogicArchive.Veltman.AxiomJ1
public import InterpretabilityLogicArchive.Veltman.AxiomJ2
public import InterpretabilityLogicArchive.Veltman.AxiomJ4
public import InterpretabilityLogicArchive.Veltman.AxiomJ5
public import InterpretabilityLogicArchive.Veltman.AxiomM
public import InterpretabilityLogicArchive.Veltman.AxiomM₀
public import InterpretabilityLogicArchive.Veltman.AxiomP
public import InterpretabilityLogicArchive.Veltman.AxiomR
public import InterpretabilityLogicArchive.Veltman.AxiomW
public import InterpretabilityLogicArchive.Veltman.Basic
public import InterpretabilityLogicArchive.Veltman.Hilbert
public import InterpretabilityLogicArchive.Veltman.Logic.CL
public import InterpretabilityLogicArchive.Veltman.Logic.IL
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1_J2
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1_J2_J5
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1_J4Plus
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1_J4Plus_J5
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J1_J5
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J2Plus
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J2Plus_J5
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J4Plus
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J4Plus_J5
public import InterpretabilityLogicArchive.Veltman.Logic.ILMinus_J5
public import InterpretabilityLogicArchive.Veltman.Logic.IL_F
public import InterpretabilityLogicArchive.Veltman.Logic.IL_M
public import InterpretabilityLogicArchive.Veltman.Logic.IL_M₀
public import InterpretabilityLogicArchive.Veltman.Logic.IL_M₀_W
public import InterpretabilityLogicArchive.Veltman.Logic.IL_P
public import InterpretabilityLogicArchive.Veltman.Logic.IL_P₀
public import InterpretabilityLogicArchive.Veltman.Logic.IL_R
public import InterpretabilityLogicArchive.Veltman.Logic.IL_R_W
public import InterpretabilityLogicArchive.Veltman.Logic.IL_W