Zulip Chat Archive

Stream: new members

Topic: constructor prefixes


view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 16:11):

It seems that I always have to disambiguate the names of constructors. E.g. I am defining

inductive binpos : Type
| one : binpos
| ext : binpos  bool  binpos

and then I try to define

def binpos2nat : binpos  
| one := 1
| (ext bs b) :=
  let n := 2*(binpos2nat bs)
  in if b then n+1 else n

but get errors, one is a variable and ext is not recognised. So I have to write

def binpos2nat : binpos  
| binpos.one := 1
| (binpos.ext bs b) :=
  let n := 2*(binpos2nat bs)
  in if b then n+1 else n

Is there a way to avoid this?

view this post on Zulip Rob Lewis (Sep 04 2020 at 16:19):

open binpos

view this post on Zulip Anne Baanen (Sep 04 2020 at 16:20):

Or if you want to copy the constructors to another namespace, export works. I think the syntax is export binpos (one ext).

view this post on Zulip Rob Lewis (Sep 04 2020 at 16:21):

If you put it inside

section
open binpos
...

end

then after the end things will revert to the original behavior.

view this post on Zulip Rob Lewis (Sep 04 2020 at 16:28):

Also note you can do some nice things with namespacing. The more canonical way to name binpos2nat is binpos.to_nat. Then you can write

inductive binpos : Type
| one : binpos
| ext : binpos  bool  binpos

namespace binpos

def to_nat : binpos  
| one := 1
| (ext bs b) :=
  let n := 2 * bs.to_nat
  in if b then n+1 else n

end binpos

#check binpos.to_nat

bs.to_nat elaborates as: "the type of bs is bin_pos, so find bin_pos.to_nat and insert bs as the first argument of type bin_pos." You can write very nice looking code with this but it's not always ideal for teaching.


Last updated: May 11 2021 at 14:11 UTC