小编bss*_*dio的帖子

我正在撰写关于依赖类型有用性的本科论文.我正在尝试构造一个容器,只能构造成一个排序列表,以便它被证明按构造排序:

import Data.So

mutual
  data SortedList : (a : Type) -> {ord : Ord a) -> Type where
    SNil : SortedList a
    SMore : (ord : Ord a) => (el: a) -> (xs : SortedList a) -> So (canPrepend el xs) -> SortedList a

  canPrepend : Ord a => a -> SortedList a -> Bool
  canPrepend el SNil = True
  canPrepend el (SMore x xs prf) = el <= x

SMore 需要运行时证明,前置元素小于或等于排序列表中的最小(第一)元素.

为了排序未排序的列表,我创建了一个函数sinsert,它接受一个排序列表并插入一个元素并返回一个排序列表:

sinsert : (ord : Ord …