ncfavier

{-# OPTIONS --no-import-sorts --erasure #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- An element of `Remember a` is a witness that `a` exists at runtime.
data Remember {ℓ} {@0 A : Type ℓ} : (@0 a : A) → Type ℓ where
  instance remember : {a : A} → Remember a

datagrok

This article is now published on my website: Prefer Subshells for Context.