Mercurial > hg > Papers > 2021 > soto-prosym
diff Paper/src/agda/abridgement.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Nov 2021 00:51:16 +0900 |
| parents | 9176dff8f38a |
| children |
line wrap: on
line diff
--- a/Paper/src/agda/abridgement.agda.replaced Sat Nov 06 20:06:24 2021 +0900 +++ b/Paper/src/agda/abridgement.agda.replaced Sun Nov 07 00:51:16 2021 +0900 @@ -4,19 +4,19 @@ record env : Set where field - a : @$\mathbb{N}$@ - b : @$\mathbb{N}$@ - c : @$\mathbb{N}$@ + a : !$\mathbb{N}$! + b : !$\mathbb{N}$! + c : !$\mathbb{N}$! open env -patternmatch-default : env @$\rightarrow$@ @$\mathbb{N}$@ +patternmatch-default : env !$\rightarrow$! !$\mathbb{N}$! patternmatch-default record { a = a ; b = b ; c = c } = c -patternmatch-extraction : env @$\rightarrow$@ @$\mathbb{N}$@ +patternmatch-extraction : env !$\rightarrow$! !$\mathbb{N}$! patternmatch-extraction env with c env patternmatch-extraction env | c = c -patternmatch-extraction' : env @$\rightarrow$@ @$\mathbb{N}$@ -patternmatch-extraction' env with c env +patternmatch-extraction!$\prime$! : env !$\rightarrow$! !$\mathbb{N}$! +patternmatch-extraction!$\prime$! env with c env ... | c = c