9a349a913a
@Kha Note that `checkRBPGreater` comment and name were incorrect. It was actually checking whether the RBP <= lower |
||
|---|---|---|
| .. | ||
| Command.lean | ||
| Level.lean | ||
| Module.lean | ||
| Parser.lean | ||
| Syntax.lean | ||
| Tactic.lean | ||
| Term.lean | ||
| Transform.lean | ||