constructor prefixes

Stream: new members

[Thorsten Altenkirch]

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]

open binpos

[Anne Baanen]

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

[Rob Lewis]

If you put it inside

section
open binpos
...

end

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

[Rob Lewis]

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.