Mercurial > hg > Members > atton > agda-proofs
view cbc/maybe-subtype.agda @ 73:a5cac9483f91
Cleanup sample
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 01 Feb 2017 05:27:05 +0000 |
parents | bd428bd6b394 |
children |
line wrap: on
line source
open import Level open import Data.Maybe open import Function using (id) open import Relation.Binary.PropositionalEquality module maybe-subtype (A : Set) where record Context : Set where open import subtype Context as N record Meta (A : Set) : Set where field context : Context maybeElem : Maybe A