type constructor constraint

Stream: lean4

[Mikhail Katkov]

Appologies for possible neglegence,

Suppose I have (many) inductive type for Capacity:

inductive Capacity where
| c1
| c2

class CapacityValue (a:Type) where
  capacity_of : Nat

Now I want to have a type that can only be constructed if its parameter is smaller than capacity, something like

inductive WithinCapacity where
| nil
| within_capacity (c:Type) (n:Nat) [CapacityValue c] [n<= CapacityValue.capacity_of c] : ...

Can I dot it? and how if I can?

[Kenny Lau]

please use #backticks to format your code

[Kenny Lau]

that should be possible, you just won't be able to use [] for it, in Lean [] and () have specialised meanings and are used for different situations

[Kenny Lau]

[] is only used for classes

[Mikhail Katkov]

So how technically I can impose constraint?

[Kenny Lau]

use ()

[Mikhail Katkov]

class CapacityValue (a:Type) where
  capacity_of : Nat

  inductive WithinCapacity where
| nil : WithinCapacity
| within_capacity (c:Type) (n:Nat) [CapacityValue c] (n<= CapacityValue.capacity_of c) : WithinCapacity

unexpected token '<='; expected ')'

[Aaron Liu]

You need to name the hypothesis

[Mikhail Katkov]

Oh! thanks a lot.

For completness, if anyone encounter that:

class CapacityValue (a:Type) where
  capacity_of : Nat

  inductive WithinCapacity where
| nil : WithinCapacity
| within_capacity (c:Type) (n:Nat) [CapacityValue c] ( _ : n<= CapacityValue.capacity_of c) : WithinCapacity

Works!