search

leanprover / reference-manual

Apache License 2.0
20 stars 3 forks source link

Transparency modes #131

Open hrmacbeth opened 1 week ago

hrmacbeth commented 1 week ago

What question should the reference manual answer?

What is the effect of different transparency modes? Both in general, but also in precise enough terms to clarify questions like "what happens if I wrap something in Lean.Meta.withReducible and then wrap that in Lean.Meta.withDefault?" (or the reverse)

What are some rules of thumb for selecting the right transparency mode when metaprogramming?

There is a little bit of information on transparency modes at 7.3.5.1. Controlling Unfolding but it doesn't yet address these kinds of more precise questions.

Additional context

Currently I often make transparency mode decisions by cargo-culting from Leo's practice, not ideal! And there are some surprising and undocumented situations in which the transparency mode designation is overriden.

david-christiansen commented 4 days ago

Thanks for this useful and actionable request!