-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.agda
34 lines (32 loc) · 1.28 KB
/
index.agda
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
module index where
-- A formalisation of Haskell B. Curry’s thesis Grundlagen der Kombinatorischen
-- Logik. See <https://www.jstor.org/stable/2370619> (part 1) and
-- <https://www.jstor.org/stable/2370716> (part 2).
import CombinatoryLogic.Equality
import CombinatoryLogic.Forest
import CombinatoryLogic.Semantics
import CombinatoryLogic.Syntax
-- A formalisation of the theory and problems presented in To Mock a Mockingbird
-- by Raymond Smullyan.
import Mockingbird.Forest
import Mockingbird.Forest.Base
import Mockingbird.Forest.Birds
import Mockingbird.Forest.Combination
import Mockingbird.Forest.Combination.Base
import Mockingbird.Forest.Combination.Properties
import Mockingbird.Forest.Combination.Vec
import Mockingbird.Forest.Combination.Vec.Base
import Mockingbird.Forest.Combination.Vec.Properties
import Mockingbird.Forest.Extensionality
import Mockingbird.Problems.Chapter09
import Mockingbird.Problems.Chapter10
import Mockingbird.Problems.Chapter11
import Mockingbird.Problems.Chapter12
import Mockingbird.Problems.Chapter13
import Mockingbird.Problems.Chapter14
import Mockingbird.Problems.Chapter15
import Mockingbird.Problems.Chapter16
import Mockingbird.Problems.Chapter17
import Mockingbird.Problems.Chapter18
import Mockingbird.Problems.Chapter19
import Mockingbird.Problems.Chapter20