Mercurial > hg > Members > atton > agda-proofs
view cbc/maybe-subtype.agda @ 77:a2e6f61d5f2b default tip
Add modus-ponens
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 09 Feb 2017 06:32:03 +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