idris2-tutorial/tutorial.ipkg at main · idris-community/idris2-tutorial · 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
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
103
104
105
106
107
108
109
110
111
112
package tutorial

authors    = "stefan-hoeck"
version    = 0.1.0
sourcedir  = "src"
depends    = base         >= 0.6.0

modules = Appendices.Neovim
        , Appendices.Projects

        , Data.HList
        , Data.List.Magic
        , Data.Union
        , Data.Validated

        , Text.CSV

        -- Chapter 1: Introduction
        , Tutorial.Intro
        , Tutorial.Intro.FirstIdrisProgram
        , Tutorial.Intro.ShapeOfADef
        -- Chapter 2: Functions Part 1
        , Tutorial.Functions1
        , Tutorial.Functions1.FunctionsWithMultipleArguments
        , Tutorial.Functions1.FunctionComposition
        , Tutorial.Functions1.HigherOrder
        , Tutorial.Functions1.Currying
        , Tutorial.Functions1.Operators
        , Tutorial.Functions1.Lambdas
        , Tutorial.Functions1.Exercises
        , Solutions.Functions1
        -- Chapter 3: Algebraic Data Types
        , Tutorial.DataTypes
        , Tutorial.DataTypes.Enumerations
        , Tutorial.DataTypes.SumTypes
        , Tutorial.DataTypes.Records
        , Tutorial.DataTypes.GenericDataTypes
        , Tutorial.DataTypes.Exercises1
        , Tutorial.DataTypes.Exercises2
        , Tutorial.DataTypes.Exercises4
        , Tutorial.DataTypes.AltSyntax
        , Solutions.DataTypes
        -- Chapter 4: Interfaces
        , Tutorial.Interfaces
        , Tutorial.Interfaces.Basics
        , Tutorial.Interfaces.More
        , Tutorial.Interfaces.Prelude
        , Solutions.Interfaces
        -- Chapter 5: Functions Part 2
        , Tutorial.Functions2
        , Tutorial.Functions2.LetBindings
        , Tutorial.Functions2.TheTruth
        , Tutorial.Functions2.Holes
        , Solutions.Functions2
        -- Chapter 6: Dependent Types
        , Tutorial.Dependent
        , Tutorial.Dependent.LengthIndexedLists
        , Tutorial.Dependent.Fin
        , Tutorial.Dependent.Comptime
        , Solutions.Dependent
        -- Chapter 7: IO: Programming With Side Effects
        , Tutorial.IO
        , Tutorial.IO.PureSideEffects
        , Tutorial.IO.DoUnsugared
        , Tutorial.IO.Files
        , Tutorial.IO.Impl
        , Solutions.IO
        -- Chapter 8: Functor and Friends
        , Tutorial.Functor
        , Tutorial.Functor.Functor
        , Tutorial.Functor.Applicative
        , Tutorial.Functor.Monad
        , Solutions.Functor
        -- Chapter 9: Recursion and Folds
        , Tutorial.Folds
        , Tutorial.Folds.Recursion
        , Tutorial.Folds.Totality
        , Tutorial.Folds.Foldable
        , Solutions.Folds
        -- Chapter 10: Effectful Traversals
        , Tutorial.Traverse
        , Tutorial.Traverse.CSV
        , Tutorial.Traverse.State
        , Tutorial.Traverse.Composition
        , Solutions.Traverse
        -- Chapter 11: Sigma Types
        , Tutorial.DPair
        , Tutorial.DPair.DPair
        , Tutorial.DPair.DNA
        , Tutorial.DPair.CSV
        , Solutions.DPair
        -- Chapter 12: Propositional Equality
        , Tutorial.Eq
        , Tutorial.Eq.Eq
        , Tutorial.Eq.ProgramsAsProofs
        , Tutorial.Eq.Void
        , Tutorial.Eq.Rewrite
        , Solutions.Eq
        -- Chapter 13: Predicates and Proof Search
        , Tutorial.Predicates
        , Tutorial.Predicates.Preconditions
        , Tutorial.Predicates.Contracts
        , Tutorial.Predicates.ErrorHandling
        , Tutorial.Predicates.Truth
        , Solutions.Predicates
        -- Chapter 14: Primitives
        , Tutorial.Prim
        , Tutorial.Prim.Prim
        , Tutorial.Prim.Strings
        , Tutorial.Prim.Integers
        , Tutorial.Prim.Refined
        , Solutions.Prim