Stream: new members
Ken Roe (Aug 11 2018 at 18:15):
If I declare values as inhabited instances, how do I reference the instances?
def cell := option ℕ def heap := ℕ → option ℕ def env := ident → ℕ instance : inhabited env := ⟨λ x, 0⟩ instance : inhabited heap := ⟨λ h, none⟩ instance : inhabited cell := ⟨none⟩ def empty_env env := env.inhabited def empty_heap : heap := heap.inhabited def empty_cell : option ℕ := cell.inhabited
The last three "def" constructs don't seem to work.
Simon Hudon (Aug 11 2018 at 18:17):
If you write
#print inhabited you should see the following appear:
@[class] structure inhabited : Sort u → Sort (max 1 u) fields: inhabited.default : Π (α : Sort u) [c : inhabited α], α
This tells you that
default env is what you want.
Last updated: May 12 2021 at 05:19 UTC