Iaia.Native.Data

Data structures that rely on Idris’ built-in recursion.

BFx : (out : boundedFixRec n f) -> BoundedFix n f

record BoundedFix n f

A recursive structure at most n nodes deep.

n

 

f

 

BFx : (out : boundedFixRec n f) -> BoundedFix n f

out : (rec : BoundedFix n f) -> boundedFixRec n f

BoundedList : Nat -> Type -> Type

Fin : Nat -> Type

boundedFixRec : Nat -> (Type -> Type) -> Type

bunfix : BoundedFix (S n) f -> f (BoundedFix n f)

weaken : Functor f => BoundedFix n f -> BoundedFix (S n) f