righ1113

open list (hiding reverse)

#check 1
#reduce head [0, 1, 2, 3]


variable {T : Type}

def snoc : list T → T → list T

righ1113

judge finite unfoldr by Idris

unfoldrが有限項か判定したい

原理的に無理なのか

/libs/contrib/Data/CoList.idr
でCoListとunfoldrは以下のように実装されている。

righ1113

module CoInductive

%default total


-- 性質Q
codata Q : Stream Nat -> Type where
  Qcons : (x:Nat) -> Q xs -> Q (x::xs)

isQ : (xs:Stream Nat) -> Q xs

righ1113

module Isort

-- > idris -p base
import Syntax.PreorderReasoning

%default total
%hide sorted


sorted : List Nat -> Bool