_∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

Question

data MinList (min : ℕ) : Set where
  []    : MinList min
  _∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

any ideal what is << >> mean?

or what the meaning of

_∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

thanks

Answer 1

There are three parameters in _∷⟪_⟫_ which are the underscores.

Number them _1 ∷ ⟪ _2 ⟫ _3 for convenience below:

The type (x : ℕ) -> min ≤ x -> MinList x -> MinList min has 3 parameters and the result type.

_1 : (x : ℕ)

_2 : min ≤ x

_3 : MinList x

The << and >> unicode are just names, nothing special. See

http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Names

and

http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Mixfix

Answer 2

Agda allows for defining "operators" (in this case, it's a type constructor) of arbitrary arity (that is, that can take an arbitrary number of arguments), the positions of each argument is indicated by an underscore, so _∷⟪_⟫_ could be written as a conventional function of three arguments:

minCons : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

and called as (for both situations)

x ::⟪ n ⟫ y

minCons x n y