-
Notifications
You must be signed in to change notification settings - Fork 0
/
Main.idr
102 lines (84 loc) · 2.34 KB
/
Main.idr
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
95
96
97
98
99
100
101
102
module Main
import PresentationKit.Slide
import PresentationKit.Presentation
import Slides.Slide.Title
import Slides.Slide.Outline
import Slides.Slide.AboutIdris
import Slides.Slide.Motivation
import Slides.Slide.Expressive
import Slides.Slide.Dependent
import Slides.Slide.ValuesValues
import Slides.Slide.TypesValues
import Slides.Slide.TypesTypes
import Slides.Slide.ValuesTypes
import Slides.Slide.Vector
import Slides.Slide.CurryHoward
import Slides.Slide.Proof
import Slides.Slide.Truth
import Slides.Slide.Falsity
import Slides.Slide.Conjunction
import Slides.Slide.Disjunction
import Slides.Slide.Implication
import Slides.Slide.Universal
import Slides.Slide.Existential
import Slides.Slide.Negation
import Slides.Slide.LEM
import Slides.Slide.LiveCoding
import Slides.Slide.Effects
import Slides.Slide.Questions
import Slides.Slide.Thanks
intro : Vect 5 Slide
intro = [ titleSlide
, outlineSlide
, aboutIdrisSlide
, motivationSlide
, expressiveSlide
]
dependentTypes : Vect 6 Slide
dependentTypes = [ dependentSlide
, valuesValuesSlide
, typesValuesSlide
, typesTypesSlide
, valuesTypesSlide
, vectorSlide
]
curryHorward : Vect 11 Slide
curryHorward = [ curryHowardSlide
, proofSlide
, truthSlide
, falsitySlide
, conjunctionSlide
, disjunctionSlide
, implicationSlide
, universalSlide
, existentialSlide
, negationSlide
, lemSlide
]
liveCoding : Vect 1 Slide
liveCoding = [liveCodingSlide]
effects : Vect 1 Slide
effects = [effectsSlide]
outro : Vect 2 Slide
outro = [ questionsSlide
, thanksSlide
]
numSlides : Nat
numSlides = with Vect sum [ length intro
, length dependentTypes
, length curryHorward
, length liveCoding
, length effects
, length outro
]
slides : Vect numSlides Slide
slides = intro
++ dependentTypes
++ curryHorward
++ liveCoding
++ effects
++ outro
main : IO ()
main = do
let presentation = initPresentation slides
render presentation