Commit d0730620 authored by Nicola Botta's avatar Nicola Botta

Changed title, fine tuned build instructions.

parent 23c63e36
# Course on functional languages and dependently typed languages
# Introduction to formal specifications and verified decision making
This repository contains teaching material for an introductory course on functional and dependently typed programming and its application to verified decision-making in the context of climate science, using the computational theory of policy advice and avoidability developed by Botta et al.([1],[2]).
This repository contains teaching material for an introduction to formal
specifications and verified decision-making, using the computational
theory of policy advice and avoidability developed by Botta et
al.([1],[2]).
## Acknowledgement
......
# Course on functional languages and dependently typed languages
# Introduction to formal specifications and verified decision making
## Summary
......@@ -27,19 +27,22 @@ Once Idris is up and running (and `idris` in your path),
- download IdrisLibs [3].
- enter `idris -i $IDRISLIBS --sourcepath $IDRISLIBS --build lectures.ipkg` to build the files
- or enter `idris -i $IDRISLIBS --sourcepath $IDRISLIBS --allow-capitalized-pattern-variables --checkpkg lectures.ipkg` to just type-check the files
- or type-check individual `.lidr` files and load them into the interactive Idris REPL (Read-Eal-Print-Loop) by typing
- Type-check individual `.lidr` files and load them into the interactive Idris REPL (Read-Eval-Print-Loop) by typing
`idris -i $IDRISLIBS --sourcepath $IDRISLIBS --allow-capitalized-pattern-variables [filename].lidr`
- or `idris -i $IDRISLIBS --sourcepath $IDRISLIBS --allow-capitalized-pattern-variables --check [filename].lidr` to only type-check [filename].
where `IDRISLIBS` is the path of `IdrisLibs` on your machine.
To remove the generated code, you can use
`idris --clean lectures.ipkg`.
## Building the .pdf files
- With `lhs2tex` [6] in your path, type `make`.
## References
[1] Botta, N., Jansson, P., Ionescu, C. (2017). Contributions to a computational theory of policy advice and avoidability. J. Funct. Program., 27, e23.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment