annotate 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
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