@@ -0,0 +1,44 @@
1+ ___ _
2+ / \ _ / \ _
3+| | | / \| | / \
4+| | | _ _ _ _ _ \_/| | ___ \_/
5+| ---/ \ \/ \ \/ \ \/ \| |/ \/ \
6+| | | -/| | || | || || || | || |
7+| | | | | | |\ | /| || || | || |
8+\_/ \_/ \___/ \_/ \_/\_/\___/| |
9+ _/ |
10+ |__/
11+ a proof automation and program construction toolkit
12+
13+
14+Pruviloj is a library of tactics that work with Idris's elaborator
15+reflection. In addition to a library of small tactics, it contains
16+code for generating eliminators for inductive datatypes and using
17+those eliminators to do induction.
18+
19+
20+Q: How do I use Pruviloj?
21+A: Call Idris with the "-p pruviloj" option and add:
22+ import Pruviloj
23+ to the top of your file. If you want to do induction, then
24+ add:
25+ import Pruviloj.Induction
26+ as well.
27+
28+
29+Q: How do I find out what's available?
30+A: Use ":browse Pruviloj.Core" after importing the library.
31+ Pruviloj.Induction exports only one name: "induction".
32+ Use ":doc" to read the built-in documentation.
33+
34+
35+Q: How do I use the tactics?
36+A: Please read the Idris documentation on elaborator reflection.
37+ The syntax to invoke a tactic script is "%runElab script". To
38+ interactively work with a hole, use ":elab holeName".
39+
40+
41+Q: Where does the name come from?
42+A: "Pruviloj" is Esperanto for "proof tools". Perhaps confusingly
43+ for Esperantists, the Pruviloj library also contains utilities
44+ for code generation.