Mercurial > hg > Members > atton > agda-proofs
changeset 43:0a780145c5ff
Define compose operator using list of subtype
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 04 Jan 2017 02:21:11 +0000 |
| parents | f7916d13e2b1 |
| children | 72cf35fb82af |
| files | cbc/named-product.agda |
| diffstat | 1 files changed, 6 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/named-product.agda Tue Jan 03 09:04:11 2017 +0000 +++ b/cbc/named-product.agda Wed Jan 04 02:21:11 2017 +0000 @@ -64,7 +64,9 @@ data CodeSegment (A B : Set) : (List Set) -> Set where - cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l + cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) + + exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context @@ -75,8 +77,8 @@ equiv-exec = refl -_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} - -> CodeSegment B C l -> CodeSegment A B ll -> CodeSegment A C (l ++ ll) -_◎_ {{da}} {{_}} {{dc}} {l = l} {ll = ll} (cs g) (cs f) = cs {l = l ++ ll} {{da}} {{dc}} (g ∘ f) +_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} + -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll)) +_◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f)