InteractionTrees/_CoqConfig at CompCertM · snu-sf/InteractionTrees · GitHub

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
-Q theories ITree

theories/Simple.v
theories/ITree.v
theories/ITreeFacts.v

theories/Basics/Basics.v
theories/Basics/Category.v
theories/Basics/CategoryOps.v
theories/Basics/CategoryTheory.v
theories/Basics/CategoryFacts.v
theories/Basics/CategorySub.v
theories/Basics/CategoryFunctor.v
theories/Basics/Monad.v
theories/Basics/MonadProp.v
theories/Basics/MonadState.v
theories/Basics/CategoryKleisli.v
theories/Basics/CategoryKleisliFacts.v
theories/Basics/Function.v
theories/Basics/FunctionFacts.v

theories/Core/ITreeDefinition.v
theories/Core/KTree.v
theories/Core/KTreeFacts.v
theories/Core/Subevent.v
theories/Core/ITreeMonad.v

theories/Eq.v
theories/Eq/Shallow.v
theories/Eq/Eq.v
theories/Eq/UpToTaus.v
theories/Eq/SimUpToTaus.v
theories/Eq/EqAxiom.v

theories/Indexed/Sum.v
theories/Indexed/Relation.v
theories/Indexed/Function.v
theories/Indexed/FunctionFacts.v

theories/Interp/Interp.v
theories/Interp/TranslateFacts.v
theories/Interp/InterpFacts.v
theories/Interp/Handler.v
theories/Interp/HandlerFacts.v
theories/Interp/Recursion.v
theories/Interp/RecursionFacts.v
theories/Interp/Traces.v

theories/Events.v
theories/Events/State.v
theories/Events/StateFacts.v
theories/Events/Reader.v
theories/Events/Writer.v
theories/Events/Exception.v
theories/Events/Nondeterminism.v
theories/Events/Map.v
theories/Events/MapDefault.v
theories/Events/MapDefaultFacts.v
theories/Events/Concurrency.v
theories/Events/Dependent.v