Skip to content

Commit

Permalink
fix readme
Browse files Browse the repository at this point in the history
  • Loading branch information
PratherConid committed Feb 20, 2024
1 parent 564469f commit 8d24ffa
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,6 @@ Lean-auto is still under development, but it's already able to solve nontrivial
* The checker is slow on large input. For example, it takes ```6s``` to typecheck the final example in ```BinderComplexity.lean```. However, this is probably acceptable for mathlib usages, because e.g ```Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean``` has two theorems that take ```4s``` to compile (but a large portion of the ```4s``` are spent on typeclass inference)
## Rules in Proof Tree
* `?<name>`: Not specified, generated in function `<name>`. This is for debug purpose only.
* `defeq <num> <name>`: The `<num>`-th definitional equality associated with definition `<name>`
* `hw <name>`: Lemmas hard-wired into Lean-auto
* `lctxInh`: Inhabitation fact from local context
Expand Down

0 comments on commit 8d24ffa

Please sign in to comment.