Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/agda/fresh_test.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 source
module fresh_test where open import Data.Nat open import Data.List.Base open import Data.List.Fresh open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) open import Data.Product open import Relation.Nary using (⌊_⌋; fromWitness) ISortedList : Set ISortedList = List!$\#$! !$\mathbb{N}$! ⌊ _>?_ ⌋ ins : ISortedList ins = 8 !$\text{::}$!!$\#$! 4 !$\text{::}$!!$\#$! 2 !$\text{::}$!!$\#$! 0 !$\text{::}$!!$\#$! []