Zulip Chat Archive

Stream: new members

Topic: referencing inhabited instances

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Aug 11 2018 at 18:17):

If you write #print inhabited you should see the following appear:

structure inhabited : Sort u  Sort (max 1 u)
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