Selector

start

Definicja struktury

definition
  let x1 be Θ1;
   .....
  let xn be Θn;
  struct (Σ1,...,Σn) Σ over a1,...,am
      (#
        σ1 -> Θ'1,
        ....
        σk -> Θ'k
      #);
end;

wprowadza konstruktory selktorów σ_i dla pól struktury nieoddziedziczonych ze struktur prefiksowych. Funktor selektorowy (konstruktor selektora) mogłaby wyglądać następująco (takiej konstrukcji nie ma w Mizarze):

definition
  let x1 be Θ1;
   .....
  let xn be Θn;
  let Σ over a1,...,am;
  sel the σi of S -> Θ'i;
end;

Funktor the σ of S służy do tworzenia termów selektorowych thr σ of τ.