Struktura

start

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

gdzie {a₁,...,a_m} ⊆ {x₁,...,x_n-1} oraz domknięcie zbioru {a₁,...,a_m} ze względu na zależność typów daje cały {x₁,...,x_n-1}.

Struktura Σ over a₁,...,a_m słuźy do tworzenia typów strukturowych Σ over τ₁,...,τ_m.

Przykład:

definition
  struct (addLoopStr,multLoopStr_0) doubleLoopStr
    (# carrier -> set,
        addF, multF -> BinOp of the carrier,
        OneF, ZeroF -> Element of the carrier
    #);
end;

Definicja struktury wprowadza drugi konstruktor - atrybut strict mówiący, że struktura nie ma innych pól poza zadeklarowanymi. Ponad to jest wprowadzana rejestracja egzystencjalna klastra: strict Σ over a₁,...,a_m.

Definicja struktury wprowadza trzeci konstruktor - agregat. Agregat możnaby zdefiniować jako (takiej konstrukcji nie ma w Mizarze)

definition
  let x1 be Θ1;
   .....
  let xn be Θn;
  let y1 be Θ'1;
        ....
  let yk be Θ'k;
  aggr Σ(#y1,...,yk#) -> strict Σ over a1,...,am;
end;

Definicja struktury wprowadza też konstruktory termów selektorowych dla nowych pól (nieodziedziczonych z struktur prefiksowych). Patrz konstruktor selektora.

Przykłady:

MSAlgebra over S (gdzie S jest non empty ManySortedSign?), mmlquery:struct, mmlquery:aggr