Trigger annotations
Trigger annotations are for forall
are explained in forall and
triggers and in more detail in Multiple variables, multiple
triggers, matching loops. Trigger annotations for exists
are explained in exists and choose.
Trigger annotations are for forall
are explained in forall and
triggers and in more detail in Multiple variables, multiple
triggers, matching loops. Trigger annotations for exists
are explained in exists and choose.