Mercurial > hg > Members > atton > agda-proofs

annotate cbc/maybe-subtype.agda @ 60:bd428bd6b394

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push/n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 00:00:40 +0000
parents 352e8a724829
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
2 open import Data.Maybe
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Function using (id)
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Binary.PropositionalEquality
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
6 module maybe-subtype (A : Set) where
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
9 record Context : Set where
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
11 open import subtype Context as N
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 record Meta (A : Set) : Set where
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 field
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
16 context : Context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
17 maybeElem : Maybe A
57
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
75f9f71f364a Trying define maybe-subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19