max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: improve docstrings for cbv and decide_cbv (#12439)

Browse source 
This PR improves docstrings for `cbv` and `decide_cbv` tactics
This commit is contained in:
Wojciech Różowski 2026-02-12 10:31:17 +00:00 • committed by GitHub
parent d9cea67e24
commit 3b2944205b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 23 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Conv.lean
View file

@ -51,8 +51,19 @@ scoped syntax (name := withAnnotateState)
/-- `skip` does nothing. -/
syntax (name := skip) "skip" : conv
/-- `cbv` performs simplification that closely mimics call-by-value evaluation,
using equations associated with definitions and the matchers. -/
/--
`cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces the target term by unfolding definitions using their defining equations and
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.
The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
This tactic is experimental and its behavior is likely to change in upcoming
releases of Lean.
-/
syntax (name := cbv) "cbv" : conv
/--

11
src/Init/Tactics.lean
View file

@ -2299,7 +2299,8 @@ macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
/--
`cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces terms by unfolding definitions using their defining equations and
applying matcher equations.
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.
`cbv` has built-in support for goals of the form `lhs = rhs`. It proceeds in
two passes:
@ -2313,6 +2314,10 @@ two passes:
(simpler) equality goal. For goals that are not equalities, `cbv` currently
leaves the goal unchanged.
The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
This tactic is experimental and its behavior is likely to change in upcoming
releases of Lean.
-/
@ -2329,6 +2334,10 @@ is a `Decidable` proposition. It proceeds in two steps:
Unlike `cbv`, `decide_cbv` is a terminal tactic: it either closes the goal or
fails.
The proofs produced by `decide_cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
This tactic is experimental and its behavior is likely to change in upcoming
releases of Lean.
-/