=== Avalog Help ===
Made by Sven Nilsen, 2020

Avalog is based on the theory of avatar extensions in path semantics:
https://github.com/advancedresearch/path_semantics/blob/master/sequences.md#avatar-extensions

Special commands:
- bye                 quits the program
- ? <pat>             search for a pattern
- prove <expr>        prove a goal
- provenr <expr>      prove a goal without reduction of the proof
- import "<file>"     imports an Avalog file
- reload              reload last import while keeping added facts and rules
- clear               clears all facts and rules
- maxsize <number>    proof search uses maximum number of facts and rules
- no maxsize          proof search uses unlimited number of facts and rules
- graph               exports expanded pairs and roles to GraphViz format
- graphf "<file>"     set GraphViz file name
- no graphf           use ".dot" after last imported Avalog file or "tmp.dot"
- echo <expr>         prints out debug format of expression
- help hide           more help about hiding and showing facts and rules
- help pairs          more help about pairs
- help roles          more help about roles
- help avatars        more help about avatars
- help rules          more help about rules
- help application    more help about application
- help eval           more help about evaluation
- help equality       more help about equality
- help inequality     more help about inequality
- help list           more help about lists
- help graph          more help about GraphViz export

Type in an expression in avatar logic, e.g. `(a, q'(b))`