Match statement in type in structure

Stream: new members

[Josiah Eldon Bills]

I am trying to define the type of potentially countably infinite binary strings. I have the following:

import order.bounded_order
import algebra.order.module

@[derive [
  has_zero, add_comm_monoid_with_one,
  canonically_ordered_comm_semiring, complete_linear_order, nontrivial,
  canonically_linear_ordered_add_monoid, has_sub, has_ordered_sub,
  linear_ordered_add_comm_monoid_with_top, decidable_eq]]
def extnat := with_top ℕ

namespace extnat

instance : inhabited extnat := ⟨0⟩

end extnat

notation (name := extnat.top) `∞` := (⊤ : extnat)


structure binstring :=
  (seq: ℕ → bool) (len: extnat) (proof: (match len with
                                        | none := true
                                        | some l := ∀n ≥ l, seq n = false
                                        end: Prop) )

Basically, finstring should be a sequence with a length, together with a proof that the sequence is 0 after the end of the length. I could probably also do this with a quotient instead, but this is the route I am trying first.

However this gives me the error "failed to register private name '_match_1', prefix has not been registered". What causes this error? What would the idiomatic way of writing the type of such a proof be? An alternative I am considering is (proof: len = ∞ ∨ (∃l: ℕ, len = l ∧ ∀n ≥ l, seq n = false))

[Kyle Miller]

FYI, your extnat is docs#enat

[Kyle Miller]

For the match expression, this seems to be a bug, but in any case I think it would be easier to work with proof: ∀n ≥ len, seq n = ff.

[Kyle Miller]

There's a coercion from nat to enat, so the statement will be vacuously true if len = ∞

[Kyle Miller]

You'll have to write it as ∀(n : ℕ), n ≥ len ∧ seq n = ff I believe (sorry, I haven't checked it in Lean)

[Josiah Eldon Bills]

All right, that makes sense