------------------------------------------------------------------------ -- An abstract specification of a semantics ------------------------------------------------------------------------ module Semantics where open import Syntax -- I don't assume any properties of the semantics. record Sem : Set1 where field -- x ⇓[ i ] v means that x _can_ terminate with the value (or -- exception) v. _⇓[_]_ : forall {t} -> Expr t -> Status -> Value -> Set -- x ⇑[ i ] means that x _can_ fail to terminate. _⇑[_] : forall {t} -> Expr t -> Status -> Set