=== Poi Reduce Help ===
Made by Sven Nilsen, 2020

Poi is based on the theory of path semantics:
https://github.com/advancedresearch/path_semantics

Special commands:
- bye            quits the program
- inline <def>   inlines definition from previous expression
- inline all     inlines all definitions from previous expression
- ``             prints separator for readability
- ` `            try again with last expression (alternative: `repeat`)
- eval <expr>    evaluates expression
- echo <expr>    prints out debug format of expression
- goal <expr>    set expression as new goal
- reset goal     reset goal
- subgoal <expr> set expression as new subgoal
- auto <expr>    prove with automated minimum Levenshtein distance
- lev            pick minimum Levenshtein distance
- auto lev       automated minimum Levenshtein distance
- inc depth      increase search depth for goal
- reset depth    reset search depth
- min depth      automated minimum depth toward goal
- pick depth     user chooses equivalence toward goal
- def <symbol>   lists definitions of symbol
- std            lists all rules in standard library
- open "<dir>"   add Poi directory
- clear dir      clear Poi directories
- <file>.poi     load Poi file as expression
- help goal      more help about goal oriented theorem proving
- help norm      more help about normal paths
- help sym       more help about symmetric paths
- help asym      more help about asymmetric paths
- help eqv       more help about equivalent expressions
- help dom       more help about domains and partial functions
- help triv      more help about trivial paths
- help ex        more help about existential paths
- help rad       more help about radians (trigonometry)
- help imag      more help about imaginary number (complex numbers)
- help eps       more help about epsilon (dual numbers)
- help deriv     more help about derivative
- help integ     more help about integral
- help list      more help about lists
- help symbol    more help about symbols vs variables
- help script    more help about scripts
- help catus     more help about Catuṣkoṭi existential lift

Type in an expression in path semantics, e.g. `and[not]`