## Stream: new members

### Topic: constructor prefixes

#### 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?

#### Rob Lewis (Sep 04 2020 at 16:19):

open binpos

#### 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).

#### 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.

#### 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