Default fields in derived structures

Stream: lean4

[Eric Wieser]

How exactly does the following work?

structure Foo where
  x : Nat

structure Bar extends Foo where
  x := 2

#check ({} : Bar)  -- { toFoo := { x := 2 } } : Bar

Without looking for the source code of Bar, how can I tell with #check / #eval that there is a default of x := 2 somewhere? #check Bar.mk reveals no such information.

[Damiano Testa]

The default field seems to produce a mdata in the resulting expression:

example : ({} : Bar) = ({ x := 3 } : Bar) := by
  inspect_lhs
/-
inspect: '{ toFoo := { x := 2 } }'

'Bar.mk' -- app
|-'Foo.mk' -- app
|   |-'[structInstDefault := true]' '2' -- mdata
|   |   |-'OfNat.ofNat' -- app
|   |   |   |-'Nat' '[]' -- const
|   |   |   |-'2' -- lit
|   |   |   |-'instOfNatNat' -- app
|   |   |   |   |-'2' -- lit
-/
  inspect_rhs
/-
inspect: '{ toFoo := { x := 3 } }'

'Bar.mk' -- app
|-'Foo.mk' -- app
|   |-'OfNat.ofNat' -- app
|   |   |-'Nat' '[]' -- const
|   |   |-'3' -- lit
|   |   |-'instOfNatNat' -- app
|   |   |   |-'3' -- lit
-/

However, if you used ({} : Bar), you probably already knew that there might have been a default field anyway...

[Damiano Testa]

Is docs#Lean.Elab.Term.StructInst.DefaultFields.findDefaultMissing? useful? I have not been able to get it to work, but it seems to give information about default fields...

[Matthew Ballard]

How are you building your docs#Lean.Elab.Term.StructInst.Struct ?

[Damiano Testa]

Yeah, that is exactly the reason I could not get it to work: it looks like everything is in place, except a constructor for Struct...

[Matthew Ballard]

I couldn’t find an ergonomic way either. I am not sure Struct is meant for public consumption. But there is some nice functionality in that file

[Damiano Testa]

Yes, virtually using Struct in my mind allowed me to do wonders with it! :upside_down:

[Eric Wieser]

Note that my question is less "how do I metaprogram this" and more "how am I expected to know that a default is available without looking at the source"?

[Eric Wieser]

(But the solution to the latter is likely to involve the former!)

[Damiano Testa]

Ah, so your question is more "how do I know that #check ({} : Bar) is going to work, if I am not allowed to look at the source". Not that I have an answer to this either, but if we could get our hands on Struct, I am sure that we could write a command that takes a name as input and returns the default values that it has...