2.2. Suppressing a definition with @[cbv_opaque]
Marking a definition @[cbv_opaque] stops cbv from exposing its body. For a
well-founded definition like countdown_opaque, this leaves cbv with nothing
to reduce, so the goal is left open.
@[cbv_opaque] def countdown_opaque (n : Nat) : List Nat :=
match n with
| 0 => [0]
| n' + 1 => (n' + 1) :: countdown_opaque n'
termination_by n
theorem countdown_opqaue_cbv
: countdown_opaque 3 = [3, 2, 1, 0] := ⊢ countdown_opaque 3 = [3, 2, 1, 0] ⊢ countdown_opaque 3 = [3, 2, 1, 0]