Idris-dev/libs/pruviloj

  ___                   _
 /   \               _ / \      _
|  |  |             / \| |     / \
|  |  | _  _ _  _ _ \_/| | ___ \_/
| ---/ \ \/ \ \/ \ \/ \| |/   \/ \
| |  |  -/| | || | || || || | || |
| |  | |  | | |\ | /| || || | || |
\_/  \_/  \___/ \_/ \_/\_/\___/| |
                              _/ |
                             |__/
     a proof automation and program construction toolkit


Pruviloj is a library of tactics that work with Idris's elaborator
reflection. In addition to a library of small tactics, it contains
code for generating eliminators for inductive datatypes and using
those eliminators to do induction.


Q: How do I use Pruviloj?
A: Call Idris with the "-p pruviloj" option and add:
      import Pruviloj
   to the top of your file. If you want to do induction, then
   add:
      import Pruviloj.Induction
   as well.


Q: How do I find out what's available?
A: Use ":browse Pruviloj.Core" after importing the library.
   Pruviloj.Induction exports only one name: "induction".
   Use ":doc" to read the built-in documentation.


Q: How do I use the tactics?
A: Please read the Idris documentation on elaborator reflection.
   The syntax to invoke a tactic script is "%runElab script". To
   interactively work with a hole, use ":elab holeName".


Q: Where does the name come from?
A: "Pruviloj" is Esperanto for "proof tools". The stress goes on
   the penultimate syllable, and in IPA the pronunciation is written
   [pruˈvi.loi̯]. Perhaps confusingly for Esperantists, the Pruviloj
   library also contains utilities for code generation.