Anand Rao

Pattern-based unfolding tactic

7

This is a tactic that allows targeted unfolding of expressions in the proof state by specifying patterns and occurrences (an idea that is due to Yaël Dillies). The file `Utils.lean`...

Hiding values of `let` declarations in Verso

5

CC: @anshula Thanks for developing Verso! We were wondering — it seems sometimes `set_option` flags work within Verso, e.g. ```lean mysection show:=false set_option linter.unusedVariables false ``` But it seems that...