Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
mpri-2.4-public
Commits
bf185fcc
Commit
bf185fcc
authored
Jan 26, 2018
by
Pierre-Évariste Dagand
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove internal noise
parent
39a4c217
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
0 additions
and
26 deletions
+0
-26
agda/Index.lagda.rst
agda/Index.lagda.rst
+0
-26
No files found.
agda/Index.lagda.rst
View file @
bf185fcc
...
...
@@ -11,32 +11,6 @@ MPRI 2.4 : Dependently-typed Functional Programming
open import 01-effectful.Monad
This course is organized as follows:
.. toctree::
:maxdepth: 1
00-agda/Warmup
01-effectful/Monad
02-dependent/Indexed
03-total/Recursion
04-generic/Desc
05-open/Problems
************************************************
Build
************************************************
You will need
* Agda (tested with version 2.5.3)
* Sphinx (tested with version 1.6.4)
Type:
``make html``
which will produce the lecture notes in ``build/html/index.html``.
************************************************
Contributing
************************************************
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment