referencing inhabited instances

Stream: new members

[Ken Roe]

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]

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.