module Meta.Brackets where

# Semantic bracket notation🔗

In many of our developments (primarily, but not limited to, those in
logic), we have a notion of a type
$T$
being a *syntactic presentation* for some other,
*semantic*, type
$S.$
In keeping with convention, we want to overload the notation
$[[e]]$
to mean “the semantic value of
$e.$”
This can be achieved with a simple notation class:

record ⟦⟧-notation {ℓ} (A : Type ℓ) : Typeω where constructor brackets field {lvl} : Level Sem : Type lvl ⟦_⟧ : A → Sem open ⟦⟧-notation ⦃...⦄ using (⟦_⟧) public {-# DISPLAY ⟦⟧-notation.⟦_⟧ f x = ⟦ x ⟧ #-}