hobbits-1.1: A library for canonically representing terms with binding

Safe HaskellSafe-Infered



Vectors indexed by a type list



data MapC f c whereSource

A MapC f c is a vector with exactly one element of type f a for each type a in the type list c.


Nil :: MapC f Nil 
:> :: MapC f c -> f a -> MapC f (c :> a) 


Show (MapC Name c) 
(NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx) 

empty :: MapC f NilSource

Create an empty MapC vector.

singleton :: f a -> MapC f (Nil :> a)Source

Create a singleton MapC vector.

lookup :: Member c a -> MapC f c -> f aSource

Look up an element of a MapC vector using a Member proof.

mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g cSource

Map a function to all elements of a MapC vector.

mapC2 :: (forall x. f x -> g x -> h x) -> MapC f c -> MapC g c -> MapC h cSource

Map a binary function to all pairs of elements of two MapC vectors.

append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)Source

Append two MapC vectors.

mkAppend :: MapC f c2 -> Append c1 c2 (c1 :++: c2)Source

Make an Append proof from any MapC vector for the second argument of the append.

mkMonoAppend :: Proxy c1 -> MapC f c2 -> Append c1 c2 (c1 :++: c2)Source

A version of mkAppend that takes in a Proxy argument.

split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)Source

Split a MapC vector into two pieces.

proxy :: MapC f c -> Proxy cSource

Create a Proxy object for the type list of a MapC vector.

members :: MapC f c -> MapC (Member c) cSource

Create a vector of proofs that each type in c is a Member of c.

replace :: MapC f c -> Member c a -> f a -> MapC f cSource

Replace a single element of a MapC vector.