pire-0.2.5

Copyright(c) Andreas Reuleaux 2015 - 2018
LicenseBSD2
MaintainerAndreas Reuleaux <rx@a-rx.info>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Syntax

Contents

Description

Pire's flavour of Pi-forall syntax, copied from Pi-forall, and adapted to Bound, Bound usage inspired by Ermine

Synopsis

Documentation

data Eps Source #

Constructors

ErasedP 
RuntimeP 
Instances
Eq Eps Source # 
Instance details

Defined in Syntax

Methods

(==) :: Eps -> Eps -> Bool #

(/=) :: Eps -> Eps -> Bool #

Ord Eps Source # 
Instance details

Defined in Syntax

Methods

compare :: Eps -> Eps -> Ordering #

(<) :: Eps -> Eps -> Bool #

(<=) :: Eps -> Eps -> Bool #

(>) :: Eps -> Eps -> Bool #

(>=) :: Eps -> Eps -> Bool #

max :: Eps -> Eps -> Eps #

min :: Eps -> Eps -> Eps #

Read Eps Source # 
Instance details

Defined in Syntax

Show Eps Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Eps -> ShowS #

show :: Eps -> String #

showList :: [Eps] -> ShowS #

data Module t a Source #

Constructors

Module 

Fields

Instances
Functor (Module t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Module t a -> Module t b #

(<$) :: a -> Module t b -> Module t a #

Foldable (Module t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Module t m -> m #

foldMap :: Monoid m => (a -> m) -> Module t a -> m #

foldr :: (a -> b -> b) -> b -> Module t a -> b #

foldr' :: (a -> b -> b) -> b -> Module t a -> b #

foldl :: (b -> a -> b) -> b -> Module t a -> b #

foldl' :: (b -> a -> b) -> b -> Module t a -> b #

foldr1 :: (a -> a -> a) -> Module t a -> a #

foldl1 :: (a -> a -> a) -> Module t a -> a #

toList :: Module t a -> [a] #

null :: Module t a -> Bool #

length :: Module t a -> Int #

elem :: Eq a => a -> Module t a -> Bool #

maximum :: Ord a => Module t a -> a #

minimum :: Ord a => Module t a -> a #

sum :: Num a => Module t a -> a #

product :: Num a => Module t a -> a #

Traversable (Module t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Module t a -> f (Module t b) #

sequenceA :: Applicative f => Module t (f a) -> f (Module t a) #

mapM :: Monad m => (a -> m b) -> Module t a -> m (Module t b) #

sequence :: Monad m => Module t (m a) -> m (Module t a) #

Eq t => Eq1 (Module t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Module t a -> Module t b -> Bool #

Ord t => Ord1 (Module t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Module t a -> Module t b -> Ordering #

Show t => Show1 (Module t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Module t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Module t a] -> ShowS #

(Eq t, Eq a) => Eq (Module t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Module t a -> Module t a -> Bool #

(/=) :: Module t a -> Module t a -> Bool #

(Ord t, Ord a) => Ord (Module t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Module t a -> Module t a -> Ordering #

(<) :: Module t a -> Module t a -> Bool #

(<=) :: Module t a -> Module t a -> Bool #

(>) :: Module t a -> Module t a -> Bool #

(>=) :: Module t a -> Module t a -> Bool #

max :: Module t a -> Module t a -> Module t a #

min :: Module t a -> Module t a -> Module t a #

(Show t, Show a) => Show (Module t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Module t a -> ShowS #

show :: Module t a -> String #

showList :: [Module t a] -> ShowS #

Pretty (Module String String) # 
Instance details

Defined in Pretty

Pretty (Module Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Module Text Text -> Doc ann #

prettyList :: [Module Text Text] -> Doc ann #

PrettyAnn (Module String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Module Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Module t a, TT t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: (Module t a, TT t a) -> (Module t a, TT t a) Source #

NoPos (Module t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Module t a -> Module t a Source #

T2S (Module Text Text, TT Text Text) (Module String String, TT String String) Source # 
Instance details

Defined in Text2String

T2S (Module Text Text) (Module String String) Source # 
Instance details

Defined in Text2String

data ModuleImport t Source #

Constructors

ModuleImport t 
Instances
Functor ModuleImport Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> ModuleImport a -> ModuleImport b #

(<$) :: a -> ModuleImport b -> ModuleImport a #

Foldable ModuleImport Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => ModuleImport m -> m #

foldMap :: Monoid m => (a -> m) -> ModuleImport a -> m #

foldr :: (a -> b -> b) -> b -> ModuleImport a -> b #

foldr' :: (a -> b -> b) -> b -> ModuleImport a -> b #

foldl :: (b -> a -> b) -> b -> ModuleImport a -> b #

foldl' :: (b -> a -> b) -> b -> ModuleImport a -> b #

foldr1 :: (a -> a -> a) -> ModuleImport a -> a #

foldl1 :: (a -> a -> a) -> ModuleImport a -> a #

toList :: ModuleImport a -> [a] #

null :: ModuleImport a -> Bool #

length :: ModuleImport a -> Int #

elem :: Eq a => a -> ModuleImport a -> Bool #

maximum :: Ord a => ModuleImport a -> a #

minimum :: Ord a => ModuleImport a -> a #

sum :: Num a => ModuleImport a -> a #

product :: Num a => ModuleImport a -> a #

Traversable ModuleImport Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> ModuleImport a -> f (ModuleImport b) #

sequenceA :: Applicative f => ModuleImport (f a) -> f (ModuleImport a) #

mapM :: Monad m => (a -> m b) -> ModuleImport a -> m (ModuleImport b) #

sequence :: Monad m => ModuleImport (m a) -> m (ModuleImport a) #

Eq t => Eq (ModuleImport t) Source # 
Instance details

Defined in Syntax

Ord t => Ord (ModuleImport t) Source # 
Instance details

Defined in Syntax

Show t => Show (ModuleImport t) Source # 
Instance details

Defined in Syntax

T2S [ModuleImport Text] [ModuleImport String] Source # 
Instance details

Defined in Text2String

T2S (ModuleImport Text) (ModuleImport String) Source # 
Instance details

Defined in Text2String

data ConstructorNames a Source #

Constructors

ConstructorNames 

Fields

Instances
Foldable ConstructorNames Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => ConstructorNames m -> m #

foldMap :: Monoid m => (a -> m) -> ConstructorNames a -> m #

foldr :: (a -> b -> b) -> b -> ConstructorNames a -> b #

foldr' :: (a -> b -> b) -> b -> ConstructorNames a -> b #

foldl :: (b -> a -> b) -> b -> ConstructorNames a -> b #

foldl' :: (b -> a -> b) -> b -> ConstructorNames a -> b #

foldr1 :: (a -> a -> a) -> ConstructorNames a -> a #

foldl1 :: (a -> a -> a) -> ConstructorNames a -> a #

toList :: ConstructorNames a -> [a] #

null :: ConstructorNames a -> Bool #

length :: ConstructorNames a -> Int #

elem :: Eq a => a -> ConstructorNames a -> Bool #

maximum :: Ord a => ConstructorNames a -> a #

minimum :: Ord a => ConstructorNames a -> a #

sum :: Num a => ConstructorNames a -> a #

product :: Num a => ConstructorNames a -> a #

Eq a => Eq (ConstructorNames a) Source # 
Instance details

Defined in Syntax

Ord a => Ord (ConstructorNames a) Source # 
Instance details

Defined in Syntax

(Read a, Ord a) => Read (ConstructorNames a) Source # 
Instance details

Defined in Syntax

Show a => Show (ConstructorNames a) Source # 
Instance details

Defined in Syntax

T2S (ConstructorNames Text) (ConstructorNames String) Source # 
Instance details

Defined in Text2String

data ConstructorDef t a Source #

A Data constructor has a name and a telescope of arguments

Constructors

ConstructorDef Delta t (Telescope t a) 
ConstructorDef' t (Telescope t a) 
Instances
Bitraversable ConstructorDef Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> ConstructorDef a b -> f (ConstructorDef c d) #

Bifoldable ConstructorDef Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => ConstructorDef m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> ConstructorDef a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> ConstructorDef a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> ConstructorDef a b -> c #

Bifunctor ConstructorDef Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> ConstructorDef a c -> ConstructorDef b d #

first :: (a -> b) -> ConstructorDef a c -> ConstructorDef b c #

second :: (b -> c) -> ConstructorDef a b -> ConstructorDef a c #

Functor (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> ConstructorDef t a -> ConstructorDef t b #

(<$) :: a -> ConstructorDef t b -> ConstructorDef t a #

Foldable (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => ConstructorDef t m -> m #

foldMap :: Monoid m => (a -> m) -> ConstructorDef t a -> m #

foldr :: (a -> b -> b) -> b -> ConstructorDef t a -> b #

foldr' :: (a -> b -> b) -> b -> ConstructorDef t a -> b #

foldl :: (b -> a -> b) -> b -> ConstructorDef t a -> b #

foldl' :: (b -> a -> b) -> b -> ConstructorDef t a -> b #

foldr1 :: (a -> a -> a) -> ConstructorDef t a -> a #

foldl1 :: (a -> a -> a) -> ConstructorDef t a -> a #

toList :: ConstructorDef t a -> [a] #

null :: ConstructorDef t a -> Bool #

length :: ConstructorDef t a -> Int #

elem :: Eq a => a -> ConstructorDef t a -> Bool #

maximum :: Ord a => ConstructorDef t a -> a #

minimum :: Ord a => ConstructorDef t a -> a #

sum :: Num a => ConstructorDef t a -> a #

product :: Num a => ConstructorDef t a -> a #

Traversable (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> ConstructorDef t a -> f (ConstructorDef t b) #

sequenceA :: Applicative f => ConstructorDef t (f a) -> f (ConstructorDef t a) #

mapM :: Monad m => (a -> m b) -> ConstructorDef t a -> m (ConstructorDef t b) #

sequence :: Monad m => ConstructorDef t (m a) -> m (ConstructorDef t a) #

Eq t => Eq1 (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> ConstructorDef t a -> ConstructorDef t b -> Bool #

Ord t => Ord1 (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> ConstructorDef t a -> ConstructorDef t b -> Ordering #

Show t => Show1 (ConstructorDef t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ConstructorDef t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ConstructorDef t a] -> ShowS #

(Eq t, Eq a) => Eq (ConstructorDef t a) Source # 
Instance details

Defined in Syntax

(Ord t, Ord a) => Ord (ConstructorDef t a) Source # 
Instance details

Defined in Syntax

(Show t, Show a) => Show (ConstructorDef t a) Source # 
Instance details

Defined in Syntax

Pretty (ConstructorDef String String) # 
Instance details

Defined in Pretty

Pretty (ConstructorDef Text Text) # 
Instance details

Defined in Pretty

PrettyAnn (ConstructorDef String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (ConstructorDef Text Text) Source # 
Instance details

Defined in Pretty

NoPos (ConstructorDef t a, TT t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: (ConstructorDef t a, TT t a) -> (ConstructorDef t a, TT t a) Source #

NoPos (ConstructorDef t a) Source # 
Instance details

Defined in NoPos

data Telescope t a Source #

Constructors

EmptyTele 
ConsP Eps (Pattern t) (Expr t a) (Telescope t a) 
Constraint (Expr t a) (Expr t a) (Telescope t a) 
Instances
Bitraversable Telescope Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Telescope a b -> f (Telescope c d) #

Bifoldable Telescope Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => Telescope m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Telescope a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Telescope a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Telescope a b -> c #

Bifunctor Telescope Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Telescope a c -> Telescope b d #

first :: (a -> b) -> Telescope a c -> Telescope b c #

second :: (b -> c) -> Telescope a b -> Telescope a c #

Functor (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Telescope t a -> Telescope t b #

(<$) :: a -> Telescope t b -> Telescope t a #

Foldable (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Telescope t m -> m #

foldMap :: Monoid m => (a -> m) -> Telescope t a -> m #

foldr :: (a -> b -> b) -> b -> Telescope t a -> b #

foldr' :: (a -> b -> b) -> b -> Telescope t a -> b #

foldl :: (b -> a -> b) -> b -> Telescope t a -> b #

foldl' :: (b -> a -> b) -> b -> Telescope t a -> b #

foldr1 :: (a -> a -> a) -> Telescope t a -> a #

foldl1 :: (a -> a -> a) -> Telescope t a -> a #

toList :: Telescope t a -> [a] #

null :: Telescope t a -> Bool #

length :: Telescope t a -> Int #

elem :: Eq a => a -> Telescope t a -> Bool #

maximum :: Ord a => Telescope t a -> a #

minimum :: Ord a => Telescope t a -> a #

sum :: Num a => Telescope t a -> a #

product :: Num a => Telescope t a -> a #

Traversable (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Telescope t a -> f (Telescope t b) #

sequenceA :: Applicative f => Telescope t (f a) -> f (Telescope t a) #

mapM :: Monad m => (a -> m b) -> Telescope t a -> m (Telescope t b) #

sequence :: Monad m => Telescope t (m a) -> m (Telescope t a) #

Eq t => Eq1 (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Telescope t a -> Telescope t b -> Bool #

Ord t => Ord1 (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Telescope t a -> Telescope t b -> Ordering #

Show t => Show1 (Telescope t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Telescope t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Telescope t a] -> ShowS #

(Eq t, Eq a) => Eq (Telescope t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Telescope t a -> Telescope t a -> Bool #

(/=) :: Telescope t a -> Telescope t a -> Bool #

(Ord t, Ord a) => Ord (Telescope t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Telescope t a -> Telescope t a -> Ordering #

(<) :: Telescope t a -> Telescope t a -> Bool #

(<=) :: Telescope t a -> Telescope t a -> Bool #

(>) :: Telescope t a -> Telescope t a -> Bool #

(>=) :: Telescope t a -> Telescope t a -> Bool #

max :: Telescope t a -> Telescope t a -> Telescope t a #

min :: Telescope t a -> Telescope t a -> Telescope t a #

(Show t, Show a) => Show (Telescope t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Telescope t a -> ShowS #

show :: Telescope t a -> String #

showList :: [Telescope t a] -> ShowS #

Pretty (Telescope String String) # 
Instance details

Defined in Pretty

Pretty (Telescope Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Telescope Text Text -> Doc ann #

prettyList :: [Telescope Text Text] -> Doc ann #

PrettyAnn (Telescope String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Telescope Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Telescope t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Telescope t a -> Telescope t a Source #

data Decl t a Source #

Constructors

Sig t (Expr t a) 
Def t (Expr t a) 
RecDef t (Expr t a) 
Data t (Telescope t a) [ConstructorDef t a] 
Instances
Bitraversable Decl Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Decl a b -> f (Decl c d) #

Bifoldable Decl Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => Decl m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Decl a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Decl a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Decl a b -> c #

Bifunctor Decl Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Decl a c -> Decl b d #

first :: (a -> b) -> Decl a c -> Decl b c #

second :: (b -> c) -> Decl a b -> Decl a c #

Functor (Decl t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Decl t a -> Decl t b #

(<$) :: a -> Decl t b -> Decl t a #

Foldable (Decl t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Decl t m -> m #

foldMap :: Monoid m => (a -> m) -> Decl t a -> m #

foldr :: (a -> b -> b) -> b -> Decl t a -> b #

foldr' :: (a -> b -> b) -> b -> Decl t a -> b #

foldl :: (b -> a -> b) -> b -> Decl t a -> b #

foldl' :: (b -> a -> b) -> b -> Decl t a -> b #

foldr1 :: (a -> a -> a) -> Decl t a -> a #

foldl1 :: (a -> a -> a) -> Decl t a -> a #

toList :: Decl t a -> [a] #

null :: Decl t a -> Bool #

length :: Decl t a -> Int #

elem :: Eq a => a -> Decl t a -> Bool #

maximum :: Ord a => Decl t a -> a #

minimum :: Ord a => Decl t a -> a #

sum :: Num a => Decl t a -> a #

product :: Num a => Decl t a -> a #

Traversable (Decl t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Decl t a -> f (Decl t b) #

sequenceA :: Applicative f => Decl t (f a) -> f (Decl t a) #

mapM :: Monad m => (a -> m b) -> Decl t a -> m (Decl t b) #

sequence :: Monad m => Decl t (m a) -> m (Decl t a) #

Eq t => Eq1 (Decl t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Decl t a -> Decl t b -> Bool #

Ord t => Ord1 (Decl t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Decl t a -> Decl t b -> Ordering #

Show t => Show1 (Decl t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Decl t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Decl t a] -> ShowS #

T2S [Decl Text Text] [Decl String String] Source # 
Instance details

Defined in Text2String

(Eq t, Eq a) => Eq (Decl t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Decl t a -> Decl t a -> Bool #

(/=) :: Decl t a -> Decl t a -> Bool #

(Ord t, Ord a) => Ord (Decl t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Decl t a -> Decl t a -> Ordering #

(<) :: Decl t a -> Decl t a -> Bool #

(<=) :: Decl t a -> Decl t a -> Bool #

(>) :: Decl t a -> Decl t a -> Bool #

(>=) :: Decl t a -> Decl t a -> Bool #

max :: Decl t a -> Decl t a -> Decl t a #

min :: Decl t a -> Decl t a -> Decl t a #

(Show t, Show a) => Show (Decl t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Decl t a -> ShowS #

show :: Decl t a -> String #

showList :: [Decl t a] -> ShowS #

Pretty (Decl String String) # 
Instance details

Defined in Pretty

Methods

pretty :: Decl String String -> Doc ann #

prettyList :: [Decl String String] -> Doc ann #

Pretty (Decl Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Decl Text Text -> Doc ann #

prettyList :: [Decl Text Text] -> Doc ann #

PrettyAnn (Decl String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Decl Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Decl t a, TT t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: (Decl t a, TT t a) -> (Decl t a, TT t a) Source #

NoPos (Decl t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Decl t a -> Decl t a Source #

T2S (Decl Text Text) (Decl String String) Source # 
Instance details

Defined in Text2String

data Arg t a Source #

Constructors

Arg Eps (Expr t a) 
Instances
Bitraversable Arg Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Arg a b -> f (Arg c d) #

Bifoldable Arg Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => Arg m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Arg a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Arg a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Arg a b -> c #

Bifunctor Arg Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Arg a c -> Arg b d #

first :: (a -> b) -> Arg a c -> Arg b c #

second :: (b -> c) -> Arg a b -> Arg a c #

Functor (Arg t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Arg t a -> Arg t b #

(<$) :: a -> Arg t b -> Arg t a #

Foldable (Arg t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Arg t m -> m #

foldMap :: Monoid m => (a -> m) -> Arg t a -> m #

foldr :: (a -> b -> b) -> b -> Arg t a -> b #

foldr' :: (a -> b -> b) -> b -> Arg t a -> b #

foldl :: (b -> a -> b) -> b -> Arg t a -> b #

foldl' :: (b -> a -> b) -> b -> Arg t a -> b #

foldr1 :: (a -> a -> a) -> Arg t a -> a #

foldl1 :: (a -> a -> a) -> Arg t a -> a #

toList :: Arg t a -> [a] #

null :: Arg t a -> Bool #

length :: Arg t a -> Int #

elem :: Eq a => a -> Arg t a -> Bool #

maximum :: Ord a => Arg t a -> a #

minimum :: Ord a => Arg t a -> a #

sum :: Num a => Arg t a -> a #

product :: Num a => Arg t a -> a #

Traversable (Arg t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Arg t a -> f (Arg t b) #

sequenceA :: Applicative f => Arg t (f a) -> f (Arg t a) #

mapM :: Monad m => (a -> m b) -> Arg t a -> m (Arg t b) #

sequence :: Monad m => Arg t (m a) -> m (Arg t a) #

Eq t => Eq1 (Arg t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Arg t a -> Arg t b -> Bool #

Ord t => Ord1 (Arg t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Arg t a -> Arg t b -> Ordering #

Show t => Show1 (Arg t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Arg t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Arg t a] -> ShowS #

(Eq t, Eq a) => Eq (Arg t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Arg t a -> Arg t a -> Bool #

(/=) :: Arg t a -> Arg t a -> Bool #

(Ord t, Ord a) => Ord (Arg t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Arg t a -> Arg t a -> Ordering #

(<) :: Arg t a -> Arg t a -> Bool #

(<=) :: Arg t a -> Arg t a -> Bool #

(>) :: Arg t a -> Arg t a -> Bool #

(>=) :: Arg t a -> Arg t a -> Bool #

max :: Arg t a -> Arg t a -> Arg t a #

min :: Arg t a -> Arg t a -> Arg t a #

(Show t, Show a) => Show (Arg t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Arg t a -> ShowS #

show :: Arg t a -> String #

showList :: [Arg t a] -> ShowS #

Pretty (Arg String String) # 
Instance details

Defined in Pretty

Methods

pretty :: Arg String String -> Doc ann #

prettyList :: [Arg String String] -> Doc ann #

Pretty (Arg Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Arg Text Text -> Doc ann #

prettyList :: [Arg Text Text] -> Doc ann #

PrettyAnn (Arg String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Arg Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Arg t a, TT t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: (Arg t a, TT t a) -> (Arg t a, TT t a) Source #

NoPos (Arg t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Arg t a -> Arg t a Source #

data Match t a Source #

Constructors

Match (Pattern t) (Scope Int (Expr t) a) 
Instances
Bitraversable Match Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Match a b -> f (Match c d) #

Bifoldable Match Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => Match m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Match a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Match a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Match a b -> c #

Bifunctor Match Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Match a c -> Match b d #

first :: (a -> b) -> Match a c -> Match b c #

second :: (b -> c) -> Match a b -> Match a c #

Functor (Match t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Match t a -> Match t b #

(<$) :: a -> Match t b -> Match t a #

Foldable (Match t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Match t m -> m #

foldMap :: Monoid m => (a -> m) -> Match t a -> m #

foldr :: (a -> b -> b) -> b -> Match t a -> b #

foldr' :: (a -> b -> b) -> b -> Match t a -> b #

foldl :: (b -> a -> b) -> b -> Match t a -> b #

foldl' :: (b -> a -> b) -> b -> Match t a -> b #

foldr1 :: (a -> a -> a) -> Match t a -> a #

foldl1 :: (a -> a -> a) -> Match t a -> a #

toList :: Match t a -> [a] #

null :: Match t a -> Bool #

length :: Match t a -> Int #

elem :: Eq a => a -> Match t a -> Bool #

maximum :: Ord a => Match t a -> a #

minimum :: Ord a => Match t a -> a #

sum :: Num a => Match t a -> a #

product :: Num a => Match t a -> a #

Traversable (Match t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Match t a -> f (Match t b) #

sequenceA :: Applicative f => Match t (f a) -> f (Match t a) #

mapM :: Monad m => (a -> m b) -> Match t a -> m (Match t b) #

sequence :: Monad m => Match t (m a) -> m (Match t a) #

Eq t => Eq1 (Match t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Match t a -> Match t b -> Bool #

Ord t => Ord1 (Match t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Match t a -> Match t b -> Ordering #

Show t => Show1 (Match t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Match t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Match t a] -> ShowS #

(Eq t, Eq a) => Eq (Match t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Match t a -> Match t a -> Bool #

(/=) :: Match t a -> Match t a -> Bool #

(Ord t, Ord a) => Ord (Match t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Match t a -> Match t a -> Ordering #

(<) :: Match t a -> Match t a -> Bool #

(<=) :: Match t a -> Match t a -> Bool #

(>) :: Match t a -> Match t a -> Bool #

(>=) :: Match t a -> Match t a -> Bool #

max :: Match t a -> Match t a -> Match t a #

min :: Match t a -> Match t a -> Match t a #

(Show t, Show a) => Show (Match t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Match t a -> ShowS #

show :: Match t a -> String #

showList :: [Match t a] -> ShowS #

Pretty (Match String String) # 
Instance details

Defined in Pretty

Methods

pretty :: Match String String -> Doc ann #

prettyList :: [Match String String] -> Doc ann #

Pretty (Match Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Match Text Text -> Doc ann #

prettyList :: [Match Text Text] -> Doc ann #

PrettyAnn (Match String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Match Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Match t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Match t a -> Match t a Source #

data Annot_ t a Source #

Constructors

Annot_ (Maybe (Expr t a)) 
Instances
Monad (Annot_ t) Source # 
Instance details

Defined in Syntax

Methods

(>>=) :: Annot_ t a -> (a -> Annot_ t b) -> Annot_ t b #

(>>) :: Annot_ t a -> Annot_ t b -> Annot_ t b #

return :: a -> Annot_ t a #

fail :: String -> Annot_ t a #

Functor (Annot_ t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Annot_ t a -> Annot_ t b #

(<$) :: a -> Annot_ t b -> Annot_ t a #

Applicative (Annot_ t) Source # 
Instance details

Defined in Syntax

Methods

pure :: a -> Annot_ t a #

(<*>) :: Annot_ t (a -> b) -> Annot_ t a -> Annot_ t b #

liftA2 :: (a -> b -> c) -> Annot_ t a -> Annot_ t b -> Annot_ t c #

(*>) :: Annot_ t a -> Annot_ t b -> Annot_ t b #

(<*) :: Annot_ t a -> Annot_ t b -> Annot_ t a #

Foldable (Annot_ t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Annot_ t m -> m #

foldMap :: Monoid m => (a -> m) -> Annot_ t a -> m #

foldr :: (a -> b -> b) -> b -> Annot_ t a -> b #

foldr' :: (a -> b -> b) -> b -> Annot_ t a -> b #

foldl :: (b -> a -> b) -> b -> Annot_ t a -> b #

foldl' :: (b -> a -> b) -> b -> Annot_ t a -> b #

foldr1 :: (a -> a -> a) -> Annot_ t a -> a #

foldl1 :: (a -> a -> a) -> Annot_ t a -> a #

toList :: Annot_ t a -> [a] #

null :: Annot_ t a -> Bool #

length :: Annot_ t a -> Int #

elem :: Eq a => a -> Annot_ t a -> Bool #

maximum :: Ord a => Annot_ t a -> a #

minimum :: Ord a => Annot_ t a -> a #

sum :: Num a => Annot_ t a -> a #

product :: Num a => Annot_ t a -> a #

Traversable (Annot_ t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Annot_ t a -> f (Annot_ t b) #

sequenceA :: Applicative f => Annot_ t (f a) -> f (Annot_ t a) #

mapM :: Monad m => (a -> m b) -> Annot_ t a -> m (Annot_ t b) #

sequence :: Monad m => Annot_ t (m a) -> m (Annot_ t a) #

type Annot t a = Maybe (Expr t a) Source #

data Expr t a Source #

Constructors

V a

variables

SizeE (Size t) 
Paren (Expr t a) 
Type

type of types

(Expr t a) :@ (Expr t a) infixl 9

application

ErasedApp (Expr t a) (Expr t a) 
Lam t (Annot t a) (Scope () (Expr t) a)

abstraction

Lam' t (Scope (Name String ()) (Expr t) a) 
Lams' [t] (Scope (Name String Int) (Expr t) a) 
ErasedLam t (Scope () (Expr t) a) 
Lams [t] (Scope Int (Expr t) a) 
LamPA (Eps, t, Annot t a) (Scope () (Expr t) a) 
LamPAs [(Eps, t, Annot t a)] (Scope Int (Expr t) a) 
Pi t (Expr t a) (Scope () (Expr t) a) 
PiP Eps (Pattern t) (Expr t a) (Scope () (Expr t) a) 
Position Delta (Expr t a) 
TrustMe (Annot t a)

an axiom TRUSTME, inhabits all types

TyUnit 
LitUnit 
TyBool 
LitBool Bool 
If (Expr t a) (Expr t a) (Expr t a) (Annot t a) 
Sigma t (Expr t a) (Scope () (Expr t) a)

sigma type `{ x : A | B }`

Prod (Expr t a) (Expr t a) (Annot t a)

introduction for sigmas `( a , b )`

Pcase (Expr t a) (t, t) (Scope Int (Expr t) a) (Annot t a)

sigma elimination form `pcase p of (x,y) -> ...`

Let t (Expr t a) (Scope () (Expr t) a) 
TyEq (Expr t a) (Expr t a) 
Refl (Annot t a) 
Subst (Expr t a) (Expr t a) (Annot t a) 
Contra (Expr t a) (Annot t a) 
TCon a [Expr t a] 
DCon t [Arg t a] (Annot t a) 
Nat Integer 
Case (Expr t a) [Match t a] (Annot t a) 
Ann (Expr t a) (Expr t a)

Annotated terms `( x : A )`

Instances
Bitraversable Expr Source # 
Instance details

Defined in Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Expr a b -> f (Expr c d) #

Bifoldable Expr Source # 
Instance details

Defined in Syntax

Methods

bifold :: Monoid m => Expr m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Expr a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Expr a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Expr a b -> c #

Bifunctor Expr Source # 
Instance details

Defined in Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> Expr a c -> Expr b d #

first :: (a -> b) -> Expr a c -> Expr b c #

second :: (b -> c) -> Expr a b -> Expr a c #

Ord a => SSubstitutable a (Expr a a) Source # 
Instance details

Defined in SSubst

Methods

sapply :: SSubst a -> Expr a a -> Expr a a Source #

fsv :: Expr a a -> Set (SVar a) Source #

Monad (Expr t) Source # 
Instance details

Defined in Syntax

Methods

(>>=) :: Expr t a -> (a -> Expr t b) -> Expr t b #

(>>) :: Expr t a -> Expr t b -> Expr t b #

return :: a -> Expr t a #

fail :: String -> Expr t a #

Functor (Expr t) Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Expr t a -> Expr t b #

(<$) :: a -> Expr t b -> Expr t a #

Applicative (Expr t) Source # 
Instance details

Defined in Syntax

Methods

pure :: a -> Expr t a #

(<*>) :: Expr t (a -> b) -> Expr t a -> Expr t b #

liftA2 :: (a -> b -> c) -> Expr t a -> Expr t b -> Expr t c #

(*>) :: Expr t a -> Expr t b -> Expr t b #

(<*) :: Expr t a -> Expr t b -> Expr t a #

Foldable (Expr t) Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Expr t m -> m #

foldMap :: Monoid m => (a -> m) -> Expr t a -> m #

foldr :: (a -> b -> b) -> b -> Expr t a -> b #

foldr' :: (a -> b -> b) -> b -> Expr t a -> b #

foldl :: (b -> a -> b) -> b -> Expr t a -> b #

foldl' :: (b -> a -> b) -> b -> Expr t a -> b #

foldr1 :: (a -> a -> a) -> Expr t a -> a #

foldl1 :: (a -> a -> a) -> Expr t a -> a #

toList :: Expr t a -> [a] #

null :: Expr t a -> Bool #

length :: Expr t a -> Int #

elem :: Eq a => a -> Expr t a -> Bool #

maximum :: Ord a => Expr t a -> a #

minimum :: Ord a => Expr t a -> a #

sum :: Num a => Expr t a -> a #

product :: Num a => Expr t a -> a #

Traversable (Expr t) Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Expr t a -> f (Expr t b) #

sequenceA :: Applicative f => Expr t (f a) -> f (Expr t a) #

mapM :: Monad m => (a -> m b) -> Expr t a -> m (Expr t b) #

sequence :: Monad m => Expr t (m a) -> m (Expr t a) #

Eq t => Eq1 (Expr t) Source # 
Instance details

Defined in Syntax

Methods

liftEq :: (a -> b -> Bool) -> Expr t a -> Expr t b -> Bool #

Ord t => Ord1 (Expr t) Source # 
Instance details

Defined in Syntax

Methods

liftCompare :: (a -> b -> Ordering) -> Expr t a -> Expr t b -> Ordering #

Show t => Show1 (Expr t) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Expr t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Expr t a] -> ShowS #

(Eq t, Eq a) => Eq (Expr t a) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Expr t a -> Expr t a -> Bool #

(/=) :: Expr t a -> Expr t a -> Bool #

(Ord t, Ord a) => Ord (Expr t a) Source # 
Instance details

Defined in Syntax

Methods

compare :: Expr t a -> Expr t a -> Ordering #

(<) :: Expr t a -> Expr t a -> Bool #

(<=) :: Expr t a -> Expr t a -> Bool #

(>) :: Expr t a -> Expr t a -> Bool #

(>=) :: Expr t a -> Expr t a -> Bool #

max :: Expr t a -> Expr t a -> Expr t a #

min :: Expr t a -> Expr t a -> Expr t a #

(Show t, Show a) => Show (Expr t a) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Expr t a -> ShowS #

show :: Expr t a -> String #

showList :: [Expr t a] -> ShowS #

Pretty (Expr String String) # 
Instance details

Defined in Pretty

Methods

pretty :: Expr String String -> Doc ann #

prettyList :: [Expr String String] -> Doc ann #

Pretty (Expr Text Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Expr Text Text -> Doc ann #

prettyList :: [Expr Text Text] -> Doc ann #

PrettyAnn (Annot Text Text) Source # 
Instance details

Defined in Pretty

PrettyAnn (Expr String String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Expr Text Text) Source # 
Instance details

Defined in Pretty

NoPos (Expr t a, TT t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: (Expr t a, TT t a) -> (Expr t a, TT t a) Source #

NoPos (Expr t a) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Expr t a -> Expr t a Source #

T2S (Expr Text Text) (Expr String String) Source # 
Instance details

Defined in Text2String

data Pattern t Source #

Constructors

PatCon t [(Eps, Pattern t)] 
PatVar t 
WildcardP t 
WildP 
Witnessed (Pattern t) 
SizeP (Size t) 
Instances
Functor Pattern Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Pattern a -> Pattern b #

(<$) :: a -> Pattern b -> Pattern a #

Foldable Pattern Source # 
Instance details

Defined in Syntax

Methods

fold :: Monoid m => Pattern m -> m #

foldMap :: Monoid m => (a -> m) -> Pattern a -> m #

foldr :: (a -> b -> b) -> b -> Pattern a -> b #

foldr' :: (a -> b -> b) -> b -> Pattern a -> b #

foldl :: (b -> a -> b) -> b -> Pattern a -> b #

foldl' :: (b -> a -> b) -> b -> Pattern a -> b #

foldr1 :: (a -> a -> a) -> Pattern a -> a #

foldl1 :: (a -> a -> a) -> Pattern a -> a #

toList :: Pattern a -> [a] #

null :: Pattern a -> Bool #

length :: Pattern a -> Int #

elem :: Eq a => a -> Pattern a -> Bool #

maximum :: Ord a => Pattern a -> a #

minimum :: Ord a => Pattern a -> a #

sum :: Num a => Pattern a -> a #

product :: Num a => Pattern a -> a #

Traversable Pattern Source # 
Instance details

Defined in Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Pattern a -> f (Pattern b) #

sequenceA :: Applicative f => Pattern (f a) -> f (Pattern a) #

mapM :: Monad m => (a -> m b) -> Pattern a -> m (Pattern b) #

sequence :: Monad m => Pattern (m a) -> m (Pattern a) #

Eq t => Eq (Pattern t) Source # 
Instance details

Defined in Syntax

Methods

(==) :: Pattern t -> Pattern t -> Bool #

(/=) :: Pattern t -> Pattern t -> Bool #

Ord t => Ord (Pattern t) Source # 
Instance details

Defined in Syntax

Methods

compare :: Pattern t -> Pattern t -> Ordering #

(<) :: Pattern t -> Pattern t -> Bool #

(<=) :: Pattern t -> Pattern t -> Bool #

(>) :: Pattern t -> Pattern t -> Bool #

(>=) :: Pattern t -> Pattern t -> Bool #

max :: Pattern t -> Pattern t -> Pattern t #

min :: Pattern t -> Pattern t -> Pattern t #

Show t => Show (Pattern t) Source # 
Instance details

Defined in Syntax

Methods

showsPrec :: Int -> Pattern t -> ShowS #

show :: Pattern t -> String #

showList :: [Pattern t] -> ShowS #

Pretty (Pattern String) # 
Instance details

Defined in Pretty

Methods

pretty :: Pattern String -> Doc ann #

prettyList :: [Pattern String] -> Doc ann #

Pretty (Pattern Text) # 
Instance details

Defined in Pretty

Methods

pretty :: Pattern Text -> Doc ann #

prettyList :: [Pattern Text] -> Doc ann #

PrettyAnn (Pattern String) Source # 
Instance details

Defined in Pretty

PrettyAnn (Pattern Text) Source # 
Instance details

Defined in Pretty

NoPos (Pattern t) Source # 
Instance details

Defined in NoPos

Methods

nopos :: Pattern t -> Pattern t Source #

bitraverseExpr :: Applicative f => (a -> f c) -> (b -> f d) -> Expr a b -> f (Expr c d) Source #

bitraverseMatch :: Applicative f => (a -> f c) -> (b -> f d) -> Match a b -> f (Match c d) Source #

bitraverseArg :: Applicative f => (a -> f c) -> (b -> f d) -> Arg a b -> f (Arg c d) Source #

bitraverseTele :: Applicative f => (a -> f c) -> (b -> f d) -> Telescope a b -> f (Telescope c d) Source #

setTraversal :: Ord b => Traversal (Set a) (Set b) a b Source #

emptyConstructorNames :: ConstructorNames Text Source #

empty set of constructor names

constrs :: forall t a. Lens' (Module t a) (ConstructorNames t) Source #

decls :: forall t a a. Lens (Module t a) (Module t a) [Decl t a] [Decl t a] Source #

imports :: forall t a. Lens' (Module t a) [ModuleImport t] Source #

mnm :: forall t a. Lens' (Module t a) t Source #

class Show3 f where Source #

Minimal complete definition

liftShowsPrec3

Methods

liftShowsPrec3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> Int -> f a b c -> ShowS Source #

liftShowList3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> [f a b c] -> ShowS Source #

Instances
Show3 (,,) Source # 
Instance details

Defined in Syntax

Methods

liftShowsPrec3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> Int -> (a, b, c) -> ShowS Source #

liftShowList3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> [(a, b, c)] -> ShowS Source #

class Eq3 g => Ord3 g where Source #

Minimal complete definition

liftCompare3

Methods

liftCompare3 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> (e -> f -> Ordering) -> g a c e -> g b d f -> Ordering Source #

Instances
Ord3 (,,) Source # 
Instance details

Defined in Syntax

Methods

liftCompare3 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> (e -> f -> Ordering) -> (a, c, e) -> (b, d, f) -> Ordering Source #

class Eq3 g where Source #

Minimal complete definition

liftEq3

Methods

liftEq3 :: (a -> b -> Bool) -> (c -> d -> Bool) -> (e -> f -> Bool) -> g a c e -> g b d f -> Bool Source #

Instances
Eq3 (,,) Source # 
Instance details

Defined in Syntax

Methods

liftEq3 :: (a -> b -> Bool) -> (c -> d -> Bool) -> (e -> f -> Bool) -> (a, c, e) -> (b, d, f) -> Bool Source #

_V :: forall t a. Prism' (Expr t a) a Source #

_SizeE :: forall t a. Prism' (Expr t a) (Size t) Source #

_Paren :: forall t a. Prism' (Expr t a) (Expr t a) Source #

_Type :: forall t a. Prism' (Expr t a) () Source #

(.:@) :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_ErasedApp :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Lam :: forall t a. Prism' (Expr t a) (t, Annot t a, Scope () (Expr t) a) Source #

_Lam' :: forall t a. Prism' (Expr t a) (t, Scope (Name String ()) (Expr t) a) Source #

_Lams' :: forall t a. Prism' (Expr t a) ([t], Scope (Name String Int) (Expr t) a) Source #

_ErasedLam :: forall t a. Prism' (Expr t a) (t, Scope () (Expr t) a) Source #

_Lams :: forall t a. Prism' (Expr t a) ([t], Scope Int (Expr t) a) Source #

_LamPA :: forall t a. Prism' (Expr t a) ((Eps, t, Annot t a), Scope () (Expr t) a) Source #

_LamPAs :: forall t a. Prism' (Expr t a) ([(Eps, t, Annot t a)], Scope Int (Expr t) a) Source #

_Pi :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_PiP :: forall t a. Prism' (Expr t a) (Eps, Pattern t, Expr t a, Scope () (Expr t) a) Source #

_Position :: forall t a. Prism' (Expr t a) (Delta, Expr t a) Source #

_TrustMe :: forall t a. Prism' (Expr t a) (Annot t a) Source #

_TyUnit :: forall t a. Prism' (Expr t a) () Source #

_LitUnit :: forall t a. Prism' (Expr t a) () Source #

_TyBool :: forall t a. Prism' (Expr t a) () Source #

_LitBool :: forall t a. Prism' (Expr t a) Bool Source #

_If :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Expr t a, Annot t a) Source #

_Sigma :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_Prod :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Annot t a) Source #

_Pcase :: forall t a. Prism' (Expr t a) (Expr t a, (t, t), Scope Int (Expr t) a, Annot t a) Source #

_Let :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_TyEq :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Refl :: forall t a. Prism' (Expr t a) (Annot t a) Source #

_Subst :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Annot t a) Source #

_Contra :: forall t a. Prism' (Expr t a) (Expr t a, Annot t a) Source #

_TCon :: forall t a. Prism' (Expr t a) (a, [Expr t a]) Source #

_DCon :: forall t a. Prism' (Expr t a) (t, [Arg t a], Annot t a) Source #

_Nat :: forall t a. Prism' (Expr t a) Integer Source #

_Case :: forall t a. Prism' (Expr t a) (Expr t a, [Match t a], Annot t a) Source #

_Ann :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Sig :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

_Def :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

_RecDef :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

_Data :: forall t a. Prism' (Decl t a) (t, Telescope t a, [ConstructorDef t a]) Source #

_PatCon :: forall t. Prism' (Pattern t) (t, [(Eps, Pattern t)]) Source #

_PatVar :: forall t. Prism' (Pattern t) t Source #

_WildcardP :: forall t. Prism' (Pattern t) t Source #

_WildP :: forall t. Prism' (Pattern t) () Source #

_Witnessed :: forall t. Prism' (Pattern t) (Pattern t) Source #

_SizeP :: forall t. Prism' (Pattern t) (Size t) Source #

Orphan instances

(Eq a, Eq b) => Eq1 ((,,) a b) Source # 
Instance details

Methods

liftEq :: (a0 -> b0 -> Bool) -> (a, b, a0) -> (a, b, b0) -> Bool #

(Ord a, Ord b) => Ord1 ((,,) a b) Source # 
Instance details

Methods

liftCompare :: (a0 -> b0 -> Ordering) -> (a, b, a0) -> (a, b, b0) -> Ordering #

(Show a, Show b) => Show1 ((,,) a b) Source # 
Instance details

Methods

liftShowsPrec :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> Int -> (a, b, a0) -> ShowS #

liftShowList :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> [(a, b, a0)] -> ShowS #