Structure fields

Stream: new members

[Nicolò Cavalleri]

If I have a structure

structure test :=
(foo : proposition)
(bar : proposition)

is there a way to do something like this (i.e. using a proof done for a previous filed without registering a lemma outside the definition)?

def hey : test :=
{ foo := by {...},
  bar := by simp [foo] }

[Floris van Doorn]

You could do

def hey : test :=
let foo : ... := ... in
{ foo := foo,
  bar := by simp [foo] }