Require Export Undecidability.FOL.FragmentSyntax.
Require Export Vector.

Local Set Implicit Arguments.

Declare Scope modelNotation.
Open Scope modelNotation.

Notation vec := t.

Section model.
    Context {Σ_funcs : funcs_signature}.
    Context {Σ_preds : preds_signature}.

    Class model :=
    {
    domain : Type;
    interp' : interp domain
    }.

    Coercion domain : model >-> Sortclass.

End model.

Arguments eval {_ _}.
Arguments i_func {_ _} _ _ _ _.
Arguments i_atom {_ _} _ _ _ _.
Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.

Arguments interp' {_ _} _, {_ _ _}.


    Notation "func ₕ[ M ] v" := (i_func _ (interp' M) func v) (at level 19).

    Notation "pred ₚ[ M ] v" := (i_atom _ (interp' M) pred v) (at level 19).

    Notation "term ₜ[ M ] env" := (eval _ (interp' M) env term) (at level 19).

    Notation "Model ⊨[_] phi" := (forall p, sat (interp' Model) p phi) (at level 21).

    Notation "Model ⊨[ ρ ] phi" := (sat (interp' Model) ρ phi) (at level 21).