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):
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
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
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