Language.Lean.List

Declares a data family List for associating a list type to different Lean values, and provides a typeclass along with associated operations for constructing and viewing Lean lists.

Documentation

data family List a

A type family for mapping a Lean value to the internal list representation.

Instances

IsList (List Name)

IsList (List Univ)

Allow (List Univ) to use OverloadedLists extensions.

IsList (List Expr)

IsList (List InductiveType)

Eq (List Name)

Eq (List Univ)

Eq (List Expr)

Eq (List InductiveType)

Show (List Name)

Show (List Univ)

Show (List Expr)

IsListIso (List Name)

IsListIso (List Univ)

IsListIso (List Expr)

IsListIso (List InductiveType)

IsLeanValue (List Name) (Ptr (List Name))

IsLeanValue (List Univ) (Ptr (List Univ))

IsLeanValue (List Expr) (Ptr (List Expr))

IsLeanValue (List InductiveType) (Ptr (List InductiveType))

type Item ListName = Name

type Item ListExpr = Expr

data List Name = ListName (ForeignPtr (List Name))

A list of names (constructor not actually exported)

data List Univ = ListUniv (ForeignPtr (List Univ))

A list of universes (constructor not actually exported)

data List Expr = ListExpr (ForeignPtr (List Expr))

A list of expressions (constructor not actually exported)

data List InductiveType = ListInductiveType (ForeignPtr (List InductiveType))

A list of inductive types (constructor not actually exported)

type Item (List Univ) = Univ

type Item (List InductiveType) = InductiveType

class IsList l => IsListIso l where

A typeclass for types that are isomorphic to lists.

This is used to provide functions for manipulating Lean's internal lists without the overhead of converting to and from Haskell lists.

Methods

nil :: l

The empty list

(<|) :: Item l -> l -> l

Cons an element to the front of a list.

listView :: l -> ListView l (Item l)

View the front of a list.

Instances

IsListIso (List Name)

IsListIso (List Univ)

IsListIso (List Expr)

IsListIso (List InductiveType)

data ListView l a

View of the front of a list

Constructors

Nil

a :< l

fromListDefault :: IsListIso l => [Item l] -> l

Convert a ordinary Haskell list to an opague list

concatList :: IsListIso l => l -> l -> l

Concatenate two lists

mapList :: (IsListIso s, IsListIso t) => (Item s -> Item t) -> s -> t

Apply a function to map one list to another.

traverseList :: (IsListIso s, IsListIso t) => Traversal s t (Item s) (Item t)

A traversal of the elements in a list.

Re-exports

class IsList l where

The IsList class and its methods are intended to be used in conjunction with the OverloadedLists extension.

Since: 4.7.0.0

Minimal complete definition

fromList, toList

Associated Types

type Item l :: *

The Item type function returns the type of items of the structure l.

Methods

fromList :: [Item l] -> l

The fromList function constructs the structure l from the given list of Item l

fromListN :: Int -> [Item l] -> l

The fromListN function takes the input list's length as a hint. Its behaviour should be equivalent to fromList. The hint can be used to construct the structure l more efficiently compared to fromList. If the given hint does not equal to the input list's length the behaviour of fromListN is not specified.

toList :: l -> [Item l]

The toList function extracts a list of Item l from the structure l. It should satisfy fromList . toList = id.

Instances

IsList Version

Since: 4.8.0.0

IsList IntSet

IsList [a]

IsList (IntMap a)

Ord a => IsList (Set a)

IsList (Seq a)

IsList (Vector a)

Prim a => IsList (Vector a)

Storable a => IsList (Vector a)

(Eq a, Hashable a) => IsList (HashSet a)

IsList (NonEmpty a)

IsList (List Name)

IsList (List Univ)

Allow (List Univ) to use OverloadedLists extensions.

IsList (List Expr)

IsList (List InductiveType)

Ord k => IsList (Map k v)

(Eq k, Hashable k) => IsList (HashMap k v)