4786e082dc
This PR updates the `inferInstanceAs` docstring to reflect current behavior: it requires an expected type from context and should not be used as a simple `inferInstance` synonym. The old example (`#check inferInstanceAs (Inhabited Nat)`) no longer works, so it's replaced with one demonstrating the intended transport use case. Additionally, renames `InstanceNormalForm.lean` to `WrapInstance.lean`, `normalizeInstance` to `wrapInstance`, and the trace class `Meta.instanceNormalForm` to `Meta.wrapInstance`, removing the "instance normal form" terminology from both documentation and code. Context: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/inferInstanceAs.20is.20broken/near/581449313 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
25 lines
569 B
Text
25 lines
569 B
Text
-- Tests that `wrapInstance` auxiliary definitions work correctly
|
|
-- when used inside a `meta` section, for both `inferInstanceAs` and `deriving`.
|
|
|
|
module
|
|
|
|
public meta import Lean.Elab.Command
|
|
|
|
public meta section
|
|
|
|
namespace Test
|
|
|
|
open Lean
|
|
|
|
-- `@[expose]` forces `wrapInstance` to create aux wrapper definitions,
|
|
-- which is where the meta marking matters.
|
|
@[expose] def Foo := Unit
|
|
deriving Inhabited
|
|
|
|
@[expose] def Bar := Name
|
|
deriving Inhabited
|
|
|
|
@[expose] def Baz := List Nat
|
|
instance : EmptyCollection Baz := inferInstanceAs (EmptyCollection (List Nat))
|
|
|
|
end Test
|