idris-1.3.2: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Core.TT

Description

TT is the core language of Idris. The language has:

  • Full dependent types
  • A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
  • Pattern matching letrec binding
  • (primitive types defined externally)

Some technical stuff:

  • Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
  • We have a simple collection of tactics which we use to elaborate source programs with implicit syntax into fully explicit terms.
Synopsis

Documentation

data AppStatus n Source #

Constructors

Complete 
MaybeHoles 
Holes [n] 
Instances
Functor AppStatus Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Eq n => Eq (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: AppStatus n -> AppStatus n -> Bool #

(/=) :: AppStatus n -> AppStatus n -> Bool #

Data n => Data (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AppStatus n -> c (AppStatus n) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AppStatus n) #

toConstr :: AppStatus n -> Constr #

dataTypeOf :: AppStatus n -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AppStatus n)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AppStatus n)) #

gmapT :: (forall b. Data b => b -> b) -> AppStatus n -> AppStatus n #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppStatus n -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppStatus n -> r #

gmapQ :: (forall d. Data d => d -> u) -> AppStatus n -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AppStatus n -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n) #

Ord n => Ord (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Show n => Show (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Generic (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (AppStatus n) :: Type -> Type #

Methods

from :: AppStatus n -> Rep (AppStatus n) x #

to :: Rep (AppStatus n) x -> AppStatus n #

ToJSON t => ToJSON (AppStatus t) Source # 
Instance details

Defined in IRTS.Portable

NFData a => NFData (AppStatus a) Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: AppStatus a -> () #

type Rep (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (AppStatus n) = D1 (MetaData "AppStatus" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "Complete" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "MaybeHoles" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Holes" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [n]))))

data ArithTy Source #

Constructors

ATInt IntTy 
ATFloat 
Instances
Eq ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArithTy -> c ArithTy #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArithTy #

toConstr :: ArithTy -> Constr #

dataTypeOf :: ArithTy -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArithTy) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArithTy) #

gmapT :: (forall b. Data b => b -> b) -> ArithTy -> ArithTy #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArithTy -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArithTy -> r #

gmapQ :: (forall d. Data d => d -> u) -> ArithTy -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ArithTy -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy #

Ord ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Show ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Generic ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ArithTy :: Type -> Type #

Methods

from :: ArithTy -> Rep ArithTy x #

to :: Rep ArithTy x -> ArithTy #

ToJSON ArithTy Source # 
Instance details

Defined in IRTS.Portable

NFData ArithTy Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ArithTy -> () #

type Rep ArithTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep ArithTy = D1 (MetaData "ArithTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "ATInt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)) :+: C1 (MetaCons "ATFloat" PrefixI False) (U1 :: Type -> Type))

data Binder b Source #

All binding forms are represented in a uniform fashion. This type only represents the types of bindings (and their values, if any); the attached identifiers are part of the Bind constructor for the TT type.

Constructors

Lam

A function binding

Fields

Pi

A binding that occurs in a function type expression, e.g. (x:Int) -> ... The binderImpl flag says whether it was a scoped implicit (i.e. forall bound) in the high level Idris, but otherwise has no relevance in TT.

Fields

Let

A binding that occurs in a let expression

Fields

NLet

NLet is an intermediate product in the evaluator that's used for temporarily naming locals during reduction. It won't occur outside the evaluator.

Fields

  • binderTy :: !b

    type annotation for bound variable

  • binderVal :: b

    value for bound variable

Hole

A hole in a term under construction in the elaborator. If this is not filled during elaboration, it is an error.

Fields

  • binderTy :: !b

    type annotation for bound variable

GHole

A saved TT hole that will later be converted to a top-level Idris metavariable applied to all elements of its local environment.

Fields

Guess

A provided value for a hole. It will later be substituted - the guess is to keep it computationally inert while working on other things if necessary.

Fields

  • binderTy :: !b

    type annotation for bound variable

  • binderVal :: b

    value for bound variable

PVar

A pattern variable (these are bound around terms that make up pattern-match clauses)

Fields

PVTy

The type of a pattern binding

Fields

  • binderTy :: !b

    type annotation for bound variable

Instances
Functor Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Foldable Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

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

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

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

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

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

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

toList :: Binder a -> [a] #

null :: Binder a -> Bool #

length :: Binder a -> Int #

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

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

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

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

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

Traversable Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

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

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

Eq b => Eq (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Binder b -> Binder b -> Bool #

(/=) :: Binder b -> Binder b -> Bool #

Data b => Data (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Binder b -> c (Binder b) #

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder b) #

toConstr :: Binder b -> Constr #

dataTypeOf :: Binder b -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder b)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder b)) #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Binder b -> Binder b #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder b -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder b -> r #

gmapQ :: (forall d. Data d => d -> u) -> Binder b -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder b -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b) #

Ord b => Ord (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Binder b -> Binder b -> Ordering #

(<) :: Binder b -> Binder b -> Bool #

(<=) :: Binder b -> Binder b -> Bool #

(>) :: Binder b -> Binder b -> Bool #

(>=) :: Binder b -> Binder b -> Bool #

max :: Binder b -> Binder b -> Binder b #

min :: Binder b -> Binder b -> Binder b #

Show b => Show (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Binder b -> ShowS #

show :: Binder b -> String #

showList :: [Binder b] -> ShowS #

Generic (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (Binder b) :: Type -> Type #

Methods

from :: Binder b -> Rep (Binder b) x #

to :: Rep (Binder b) x -> Binder b #

ToJSON t => ToJSON (Binder t) Source # 
Instance details

Defined in IRTS.Portable

Binary b => Binary (Binder b) Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Binder b -> Put #

get :: Get (Binder b) #

putList :: [Binder b] -> Put #

NFData b => NFData (Binder b) Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Binder b -> () #

type Rep (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (Binder b) = D1 (MetaData "Binder" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((C1 (MetaCons "Lam" PrefixI True) (S1 (MetaSel (Just "binderCount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount) :*: S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)) :+: C1 (MetaCons "Pi" PrefixI True) ((S1 (MetaSel (Just "binderCount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount) :*: S1 (MetaSel (Just "binderImpl") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ImplicitInfo))) :*: (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b) :*: S1 (MetaSel (Just "binderKind") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)))) :+: (C1 (MetaCons "Let" PrefixI True) (S1 (MetaSel (Just "binderCount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount) :*: (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b) :*: S1 (MetaSel (Just "binderVal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b))) :+: C1 (MetaCons "NLet" PrefixI True) (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b) :*: S1 (MetaSel (Just "binderVal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b)))) :+: ((C1 (MetaCons "Hole" PrefixI True) (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)) :+: C1 (MetaCons "GHole" PrefixI True) (S1 (MetaSel (Just "envlen") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: (S1 (MetaSel (Just "localnames") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]) :*: S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)))) :+: (C1 (MetaCons "Guess" PrefixI True) (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b) :*: S1 (MetaSel (Just "binderVal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b)) :+: (C1 (MetaCons "PVar" PrefixI True) (S1 (MetaSel (Just "binderCount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount) :*: S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)) :+: C1 (MetaCons "PVTy" PrefixI True) (S1 (MetaSel (Just "binderTy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b))))))

data Const Source #

Instances
Eq Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Const -> c Const #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Const #

toConstr :: Const -> Constr #

dataTypeOf :: Const -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Const) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Const) #

gmapT :: (forall b. Data b => b -> b) -> Const -> Const #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r #

gmapQ :: (forall d. Data d => d -> u) -> Const -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Const -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Const -> m Const #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const #

Ord Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Const -> Const -> Ordering #

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

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

(>) :: Const -> Const -> Bool #

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

max :: Const -> Const -> Const #

min :: Const -> Const -> Const #

Show Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Const -> ShowS #

show :: Const -> String #

showList :: [Const] -> ShowS #

Generic Const Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Const :: Type -> Type #

Methods

from :: Const -> Rep Const x #

to :: Rep Const x -> Const #

ToJSON Const Source # 
Instance details

Defined in IRTS.Portable

Binary Const Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Const -> Put #

get :: Get Const #

putList :: [Const] -> Put #

NFData Const Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Const -> () #

type Rep Const Source # 
Instance details

Defined in Idris.Core.TT

type Rep Const = D1 (MetaData "Const" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((C1 (MetaCons "I" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "BI" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "Fl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Double)))) :+: ((C1 (MetaCons "Ch" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Char)) :+: C1 (MetaCons "Str" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "B8" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word8)) :+: C1 (MetaCons "B16" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word16))))) :+: (((C1 (MetaCons "B32" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word32)) :+: C1 (MetaCons "B64" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word64))) :+: (C1 (MetaCons "AType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy)) :+: C1 (MetaCons "StrType" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "WorldType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TheWorld" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "VoidType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Forgot" PrefixI False) (U1 :: Type -> Type)))))

type Ctxt a = Map Name (Map Name a) Source #

Contexts allow us to map names to things. A root name maps to a collection of things in different namespaces with that name.

data ConstraintFC Source #

Constructors

ConstraintFC 

Fields

Instances
Eq ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Data ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConstraintFC -> c ConstraintFC #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConstraintFC #

toConstr :: ConstraintFC -> Constr #

dataTypeOf :: ConstraintFC -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConstraintFC) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstraintFC) #

gmapT :: (forall b. Data b => b -> b) -> ConstraintFC -> ConstraintFC #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConstraintFC -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConstraintFC -> r #

gmapQ :: (forall d. Data d => d -> u) -> ConstraintFC -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstraintFC -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC #

Ord ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Show ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Generic ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ConstraintFC :: Type -> Type #

Binary ConstraintFC Source # 
Instance details

Defined in Idris.Core.Binary

NFData ConstraintFC Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ConstraintFC -> () #

type Rep ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

type Rep ConstraintFC = D1 (MetaData "ConstraintFC" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "ConstraintFC" PrefixI True) (S1 (MetaSel (Just "uconstraint") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UConstraint) :*: S1 (MetaSel (Just "ufc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC)))

data DataOpt Source #

Data declaration options

Constructors

Codata

Set if the the data-type is coinductive

DataErrRev 
Instances
Eq DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Show DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Generic DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep DataOpt :: Type -> Type #

Methods

from :: DataOpt -> Rep DataOpt x #

to :: Rep DataOpt x -> DataOpt #

Binary DataOpt Source # 
Instance details

Defined in Idris.IBC

Methods

put :: DataOpt -> Put #

get :: Get DataOpt #

putList :: [DataOpt] -> Put #

NFData DataOpt Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DataOpt -> () #

type Rep DataOpt Source # 
Instance details

Defined in Idris.Core.TT

type Rep DataOpt = D1 (MetaData "DataOpt" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "Codata" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "DataErrRev" PrefixI False) (U1 :: Type -> Type))

data Datatype n Source #

Constructors

Data 

Fields

Instances
Functor Datatype Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Eq n => Eq (Datatype n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Datatype n -> Datatype n -> Bool #

(/=) :: Datatype n -> Datatype n -> Bool #

(Show n, Eq n) => Show (Datatype n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Datatype n -> ShowS #

show :: Datatype n -> String #

showList :: [Datatype n] -> ShowS #

type EnvTT n = [(n, RigCount, Binder (TT n))] Source #

data Err' t Source #

Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.

Instances
Functor Err' Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> Err' a -> Err' b #

(<$) :: a -> Err' b -> Err' a #

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS #

show :: Err -> String #

showList :: [Err] -> ShowS #

NFData Err Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> () #

Eq t => Eq (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Err' t -> Err' t -> Bool #

(/=) :: Err' t -> Err' t -> Bool #

Data t => Data (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Err' t -> c (Err' t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Err' t) #

toConstr :: Err' t -> Constr #

dataTypeOf :: Err' t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Err' t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Err' t)) #

gmapT :: (forall b. Data b => b -> b) -> Err' t -> Err' t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Err' t -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Err' t -> r #

gmapQ :: (forall d. Data d => d -> u) -> Err' t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Err' t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t) #

Ord t => Ord (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Err' t -> Err' t -> Ordering #

(<) :: Err' t -> Err' t -> Bool #

(<=) :: Err' t -> Err' t -> Bool #

(>) :: Err' t -> Err' t -> Bool #

(>=) :: Err' t -> Err' t -> Bool #

max :: Err' t -> Err' t -> Err' t #

min :: Err' t -> Err' t -> Err' t #

Generic (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (Err' t) :: Type -> Type #

Methods

from :: Err' t -> Rep (Err' t) x #

to :: Rep (Err' t) x -> Err' t #

Binary a => Binary (Err' a) Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Err' a -> Put #

get :: Get (Err' a) #

putList :: [Err' a] -> Put #

MonadException m => MonadException (ExceptT Err m) Source # 
Instance details

Defined in Idris.Output

Methods

controlIO :: (RunIO (ExceptT Err m) -> IO (ExceptT Err m a)) -> ExceptT Err m a #

type Rep (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (Err' t) = D1 (MetaData "Err'" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((((C1 (MetaCons "Msg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "InternalMsg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "CantUnify" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t, Maybe Provenance)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t, Maybe Provenance)))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t)]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) :+: (C1 (MetaCons "InfiniteUnify" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t)]))) :+: C1 (MetaCons "CantConvert" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t)])))))) :+: ((C1 (MetaCons "CantSolveGoal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t)])) :+: (C1 (MetaCons "UnifyScope" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t)]))) :+: C1 (MetaCons "CantInferType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: (C1 (MetaCons "NonFunctionType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "NotEquality" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "TooManyArguments" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)))))) :+: (((C1 (MetaCons "CantIntroduce" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "NoSuchVariable" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :+: (C1 (MetaCons "WithFnType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "NoTypeDecl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "NotInjective" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))))) :+: ((C1 (MetaCons "CantResolve" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t)))) :+: (C1 (MetaCons "InvalidTCArg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "CantResolveAlts" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name])))) :+: (C1 (MetaCons "NoValidAlts" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name])) :+: (C1 (MetaCons "IncompleteTerm" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "UniverseError" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UExp)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Int, Int)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Int, Int)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ConstraintFC]))))))))) :+: ((((C1 (MetaCons "UniqueError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Universe) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "UniqueKindError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Universe) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :+: (C1 (MetaCons "ProgramLineComment" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Inaccessible" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "UnknownImplicit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))))) :+: ((C1 (MetaCons "CantMatch" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "NonCollapsiblePostulate" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "AlreadyDefined" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)))) :+: (C1 (MetaCons "ProofSearchFail" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))) :+: (C1 (MetaCons "NoRewriting" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :+: C1 (MetaCons "At" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))))))) :+: (((C1 (MetaCons "Elaborating" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe t)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t)))) :+: C1 (MetaCons "ElaboratingArg" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, Name)]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))))) :+: (C1 (MetaCons "ProviderError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "LoadingFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))) :+: C1 (MetaCons "ReflectionError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[ErrorReportPart]]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t)))))) :+: ((C1 (MetaCons "ReflectionFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))) :+: (C1 (MetaCons "ElabScriptDebug" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ErrorReportPart]) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, t, [(Name, Binder t)])]))) :+: C1 (MetaCons "ElabScriptStuck" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))) :+: (C1 (MetaCons "RunningElabScript" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Err' t))) :+: (C1 (MetaCons "ElabScriptStaging" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "FancyMsg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ErrorReportPart]))))))))

data ErrorReportPart Source #

Used for error reflection

Instances
Eq ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Data ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ErrorReportPart -> c ErrorReportPart #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ErrorReportPart #

toConstr :: ErrorReportPart -> Constr #

dataTypeOf :: ErrorReportPart -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ErrorReportPart) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ErrorReportPart) #

gmapT :: (forall b. Data b => b -> b) -> ErrorReportPart -> ErrorReportPart #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ErrorReportPart -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ErrorReportPart -> r #

gmapQ :: (forall d. Data d => d -> u) -> ErrorReportPart -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ErrorReportPart -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart #

Ord ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Show ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Generic ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ErrorReportPart :: Type -> Type #

Binary ErrorReportPart Source # 
Instance details

Defined in Idris.Core.Binary

NFData ErrorReportPart Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ErrorReportPart -> () #

type Rep ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

data FC Source #

Source location. These are typically produced by withExtent

Constructors

FC 

Fields

NoFC

Locations for machine-generated terms

FileFC

Locations with file only

Fields

Instances
Eq FC Source #

Ignore source location equality (so deriving classes do not compare FCs)

Instance details

Defined in Idris.Core.TT

Methods

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

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

Data FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FC -> c FC #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FC #

toConstr :: FC -> Constr #

dataTypeOf :: FC -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FC) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FC) #

gmapT :: (forall b. Data b => b -> b) -> FC -> FC #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FC -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FC -> r #

gmapQ :: (forall d. Data d => d -> u) -> FC -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FC -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FC -> m FC #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FC -> m FC #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FC -> m FC #

Ord FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: FC -> FC -> Ordering #

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

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

(>) :: FC -> FC -> Bool #

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

max :: FC -> FC -> FC #

min :: FC -> FC -> FC #

Show FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> FC -> ShowS #

show :: FC -> String #

showList :: [FC] -> ShowS #

Generic FC Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep FC :: Type -> Type #

Methods

from :: FC -> Rep FC x #

to :: Rep FC x -> FC #

Semigroup FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

(<>) :: FC -> FC -> FC #

sconcat :: NonEmpty FC -> FC #

stimes :: Integral b => b -> FC -> FC #

Monoid FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

mempty :: FC #

mappend :: FC -> FC -> FC #

mconcat :: [FC] -> FC #

Binary FC Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: FC -> Put #

get :: Get FC #

putList :: [FC] -> Put #

NFData FC Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: FC -> () #

SExpable FC Source # 
Instance details

Defined in Idris.IdeMode

Methods

toSExp :: FC -> SExp Source #

type Rep FC Source # 
Instance details

Defined in Idris.Core.TT

newtype FC' Source #

FC with equality

Constructors

FC' 

Fields

Instances
Eq FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: FC' -> FC' -> Bool #

(/=) :: FC' -> FC' -> Bool #

Data FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FC' -> c FC' #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FC' #

toConstr :: FC' -> Constr #

dataTypeOf :: FC' -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FC') #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FC') #

gmapT :: (forall b. Data b => b -> b) -> FC' -> FC' #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FC' -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FC' -> r #

gmapQ :: (forall d. Data d => d -> u) -> FC' -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FC' -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FC' -> m FC' #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FC' -> m FC' #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FC' -> m FC' #

Ord FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: FC' -> FC' -> Ordering #

(<) :: FC' -> FC' -> Bool #

(<=) :: FC' -> FC' -> Bool #

(>) :: FC' -> FC' -> Bool #

(>=) :: FC' -> FC' -> Bool #

max :: FC' -> FC' -> FC' #

min :: FC' -> FC' -> FC' #

Show FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> FC' -> ShowS #

show :: FC' -> String #

showList :: [FC'] -> ShowS #

Generic FC' Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep FC' :: Type -> Type #

Methods

from :: FC' -> Rep FC' x #

to :: Rep FC' x -> FC' #

Binary FC' Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: FC' -> Put #

get :: Get FC' #

putList :: [FC'] -> Put #

NFData FC' Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: FC' -> () #

type Rep FC' Source # 
Instance details

Defined in Idris.Core.TT

type Rep FC' = D1 (MetaData "FC'" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" True) (C1 (MetaCons "FC'" PrefixI True) (S1 (MetaSel (Just "unwrapFC") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC)))

data ImplicitInfo Source #

Constructors

Impl 
Instances
Eq ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Data ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImplicitInfo -> c ImplicitInfo #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImplicitInfo #

toConstr :: ImplicitInfo -> Constr #

dataTypeOf :: ImplicitInfo -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ImplicitInfo) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImplicitInfo) #

gmapT :: (forall b. Data b => b -> b) -> ImplicitInfo -> ImplicitInfo #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImplicitInfo -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImplicitInfo -> r #

gmapQ :: (forall d. Data d => d -> u) -> ImplicitInfo -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImplicitInfo -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo #

Ord ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Show ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Generic ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ImplicitInfo :: Type -> Type #

ToJSON ImplicitInfo Source # 
Instance details

Defined in IRTS.Portable

Binary ImplicitInfo Source # 
Instance details

Defined in Idris.Core.Binary

NFData ImplicitInfo Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ImplicitInfo -> () #

type Rep ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

type Rep ImplicitInfo = D1 (MetaData "ImplicitInfo" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "Impl" PrefixI True) (S1 (MetaSel (Just "tcimplementation") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Just "toplevel_imp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "machine_gen") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))

data IntTy Source #

Instances
Eq IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IntTy -> c IntTy #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IntTy #

toConstr :: IntTy -> Constr #

dataTypeOf :: IntTy -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IntTy) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntTy) #

gmapT :: (forall b. Data b => b -> b) -> IntTy -> IntTy #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntTy -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntTy -> r #

gmapQ :: (forall d. Data d => d -> u) -> IntTy -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IntTy -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy #

Ord IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: IntTy -> IntTy -> Ordering #

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

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

(>) :: IntTy -> IntTy -> Bool #

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

max :: IntTy -> IntTy -> IntTy #

min :: IntTy -> IntTy -> IntTy #

Show IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> IntTy -> ShowS #

show :: IntTy -> String #

showList :: [IntTy] -> ShowS #

Generic IntTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep IntTy :: Type -> Type #

Methods

from :: IntTy -> Rep IntTy x #

to :: Rep IntTy x -> IntTy #

ToJSON IntTy Source # 
Instance details

Defined in IRTS.Portable

NFData IntTy Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: IntTy -> () #

type Rep IntTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep IntTy = D1 (MetaData "IntTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "ITFixed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NativeTy)) :+: C1 (MetaCons "ITNative" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "ITBig" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "ITChar" PrefixI False) (U1 :: Type -> Type)))

data Name Source #

Names are hierarchies of strings, describing scope (so no danger of duplicate names, but need to be careful on lookup).

Constructors

UN !Text

User-provided name

NS !Name [Text]

Root, namespaces

MN !Int !Text

Machine chosen names

SN !SpecialName

Decorated function names

SymRef Int

Reference to IBC file symbol table (used during serialisation)

Instances
Eq Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name #

toConstr :: Name -> Constr #

dataTypeOf :: Name -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) #

gmapT :: (forall b. Data b => b -> b) -> Name -> Name #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r #

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #

Ord Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Name -> Name -> Ordering #

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

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

(>) :: Name -> Name -> Bool #

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

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Show Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS #

show :: Err -> String #

showList :: [Err] -> ShowS #

Generic Name Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Name :: Type -> Type #

Methods

from :: Name -> Rep Name x #

to :: Rep Name x -> Name #

ToJSON Name Source # 
Instance details

Defined in IRTS.Portable

Binary Name Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Name -> Put #

get :: Get Name #

putList :: [Name] -> Put #

Binary CaseAlt Source # 
Instance details

Defined in Idris.IBC

Methods

put :: CaseAlt -> Put #

get :: Get CaseAlt #

putList :: [CaseAlt] -> Put #

Binary SC Source # 
Instance details

Defined in Idris.IBC

Methods

put :: SC -> Put #

get :: Get SC #

putList :: [SC] -> Put #

NFData Name Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Name -> () #

NFData Err Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> () #

TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

SExpable Name Source # 
Instance details

Defined in Idris.IdeMode

Methods

toSExp :: Name -> SExp Source #

Binary (TT Name) Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: TT Name -> Put #

get :: Get (TT Name) #

putList :: [TT Name] -> Put #

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

MonadException m => MonadException (ExceptT Err m) Source # 
Instance details

Defined in Idris.Output

Methods

controlIO :: (RunIO (ExceptT Err m) -> IO (ExceptT Err m a)) -> ExceptT Err m a #

type Rep Name Source # 
Instance details

Defined in Idris.Core.TT

data NameOutput Source #

Output annotation for pretty-printed name - decides colour

Instances
Eq NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Ord NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Show NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Generic NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NameOutput :: Type -> Type #

NFData NameOutput Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NameOutput -> () #

SExpable NameOutput Source # 
Instance details

Defined in Idris.IdeMode

type Rep NameOutput Source # 
Instance details

Defined in Idris.Core.TT

type Rep NameOutput = D1 (MetaData "NameOutput" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "TypeOutput" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "FunOutput" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "DataOutput" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "MetavarOutput" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PostulateOutput" PrefixI False) (U1 :: Type -> Type))))

data NameType Source #

Constructors

Bound 
Ref 
DCon

Data constructor

Fields

TCon

Type constructor

Fields

Instances
Eq NameType Source # 
Instance details

Defined in Idris.Core.TT

Data NameType Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameType -> c NameType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameType #

toConstr :: NameType -> Constr #

dataTypeOf :: NameType -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameType) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameType) #

gmapT :: (forall b. Data b => b -> b) -> NameType -> NameType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameType -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameType -> r #

gmapQ :: (forall d. Data d => d -> u) -> NameType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameType -> m NameType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameType -> m NameType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameType -> m NameType #

Ord NameType Source # 
Instance details

Defined in Idris.Core.TT

Show NameType Source # 
Instance details

Defined in Idris.Core.TT

Generic NameType Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NameType :: Type -> Type #

Methods

from :: NameType -> Rep NameType x #

to :: Rep NameType x -> NameType #

ToJSON NameType Source # 
Instance details

Defined in IRTS.Portable

Binary NameType Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: NameType -> Put #

get :: Get NameType #

putList :: [NameType] -> Put #

NFData NameType Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NameType -> () #

type Rep NameType Source # 
Instance details

Defined in Idris.Core.TT

data NativeTy Source #

Constructors

IT8 
IT16 
IT32 
IT64 
Instances
Enum NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Eq NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Data NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NativeTy -> c NativeTy #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NativeTy #

toConstr :: NativeTy -> Constr #

dataTypeOf :: NativeTy -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NativeTy) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NativeTy) #

gmapT :: (forall b. Data b => b -> b) -> NativeTy -> NativeTy #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NativeTy -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NativeTy -> r #

gmapQ :: (forall d. Data d => d -> u) -> NativeTy -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NativeTy -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy #

Ord NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Show NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Generic NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NativeTy :: Type -> Type #

Methods

from :: NativeTy -> Rep NativeTy x #

to :: Rep NativeTy x -> NativeTy #

NFData NativeTy Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NativeTy -> () #

type Rep NativeTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep NativeTy = D1 (MetaData "NativeTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "IT8" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "IT16" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "IT32" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "IT64" PrefixI False) (U1 :: Type -> Type)))

data OutputAnnotation Source #

Output annotations for pretty-printing

Constructors

AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

^ The name, classification, docs overview, and pretty-printed type

AnnBoundName Name Bool

^ The name and whether it is implicit

AnnConst Const 
AnnData String String

type, doc overview

AnnType String String

name, doc overview

AnnKeyword 
AnnFC FC 
AnnTextFmt TextFormatting 
AnnLink String

A link to this URL

AnnTerm [(Name, Bool)] (TT Name)

pprint bound vars, original term

AnnSearchResult Ordering

more general, isomorphic, or more specific

AnnErr Err 
AnnNamespace [Text] (Maybe FilePath)

A namespace (e.g. on an import line or in a namespace declaration). Stored starting at the root, with the hierarchy fully resolved. If a file path is present, then the namespace represents a module imported from that file.

AnnQuasiquote 
AnnAntiquote 
AnnSyntax String

type of syntax element: backslash or braces etc.

Instances
Eq OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Ord OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Show OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Generic OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep OutputAnnotation :: Type -> Type #

NFData OutputAnnotation Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: OutputAnnotation -> () #

SExpable OutputAnnotation Source # 
Instance details

Defined in Idris.IdeMode

type Rep OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

type Rep OutputAnnotation = D1 (MetaData "OutputAnnotation" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((((C1 (MetaCons "AnnName" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe NameOutput))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))) :+: C1 (MetaCons "AnnBoundName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) :+: (C1 (MetaCons "AnnConst" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Const)) :+: C1 (MetaCons "AnnData" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "AnnType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "AnnKeyword" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "AnnFC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC)) :+: C1 (MetaCons "AnnTextFmt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TextFormatting))))) :+: (((C1 (MetaCons "AnnLink" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "AnnTerm" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, Bool)]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT Name)))) :+: (C1 (MetaCons "AnnSearchResult" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ordering)) :+: C1 (MetaCons "AnnErr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Err)))) :+: ((C1 (MetaCons "AnnNamespace" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Text]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe FilePath))) :+: C1 (MetaCons "AnnQuasiquote" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "AnnAntiquote" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "AnnSyntax" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))

data Provenance Source #

Instances
Eq Provenance Source # 
Instance details

Defined in Idris.Core.TT

Data Provenance Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Provenance -> c Provenance #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Provenance #

toConstr :: Provenance -> Constr #

dataTypeOf :: Provenance -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Provenance) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance) #

gmapT :: (forall b. Data b => b -> b) -> Provenance -> Provenance #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r #

gmapQ :: (forall d. Data d => d -> u) -> Provenance -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Provenance -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

Ord Provenance Source # 
Instance details

Defined in Idris.Core.TT

Show Provenance Source # 
Instance details

Defined in Idris.Core.TT

Generic Provenance Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Provenance :: Type -> Type #

Binary Provenance Source # 
Instance details

Defined in Idris.Core.Binary

NFData Provenance Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Provenance -> () #

type Rep Provenance Source # 
Instance details

Defined in Idris.Core.TT

type Rep Provenance = D1 (MetaData "Provenance" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "ExpectedType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TooManyArgs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Term))) :+: (C1 (MetaCons "InferredVal" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "GivenVal" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SourceTerm" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Term)))))

data Raw Source #

Instances
Eq Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Raw -> c Raw #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Raw #

toConstr :: Raw -> Constr #

dataTypeOf :: Raw -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Raw) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Raw) #

gmapT :: (forall b. Data b => b -> b) -> Raw -> Raw #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Raw -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Raw -> r #

gmapQ :: (forall d. Data d => d -> u) -> Raw -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Raw -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Raw -> m Raw #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Raw -> m Raw #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Raw -> m Raw #

Ord Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Raw -> Raw -> Ordering #

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

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

(>) :: Raw -> Raw -> Bool #

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

max :: Raw -> Raw -> Raw #

min :: Raw -> Raw -> Raw #

Show Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Raw -> ShowS #

show :: Raw -> String #

showList :: [Raw] -> ShowS #

Generic Raw Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Raw :: Type -> Type #

Methods

from :: Raw -> Rep Raw x #

to :: Rep Raw x -> Raw #

Binary Raw Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Raw -> Put #

get :: Get Raw #

putList :: [Raw] -> Put #

NFData Raw Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Raw -> () #

type Rep Raw Source # 
Instance details

Defined in Idris.Core.TT

data RigCount Source #

Constructors

Rig0 
Rig1 
RigW 
Instances
Eq RigCount Source # 
Instance details

Defined in Idris.Core.TT

Data RigCount Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RigCount -> c RigCount #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RigCount #

toConstr :: RigCount -> Constr #

dataTypeOf :: RigCount -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RigCount) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RigCount) #

gmapT :: (forall b. Data b => b -> b) -> RigCount -> RigCount #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RigCount -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RigCount -> r #

gmapQ :: (forall d. Data d => d -> u) -> RigCount -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RigCount -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount #

Ord RigCount Source # 
Instance details

Defined in Idris.Core.TT

Show RigCount Source # 
Instance details

Defined in Idris.Core.TT

Generic RigCount Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep RigCount :: Type -> Type #

Methods

from :: RigCount -> Rep RigCount x #

to :: Rep RigCount x -> RigCount #

ToJSON RigCount Source # 
Instance details

Defined in IRTS.Portable

Binary RigCount Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: RigCount -> Put #

get :: Get RigCount #

putList :: [RigCount] -> Put #

NFData RigCount Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: RigCount -> () #

type Rep RigCount Source # 
Instance details

Defined in Idris.Core.TT

type Rep RigCount = D1 (MetaData "RigCount" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "Rig0" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Rig1" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "RigW" PrefixI False) (U1 :: Type -> Type)))

data SpecialName Source #

Instances
Eq SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Data SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpecialName -> c SpecialName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpecialName #

toConstr :: SpecialName -> Constr #

dataTypeOf :: SpecialName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpecialName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecialName) #

gmapT :: (forall b. Data b => b -> b) -> SpecialName -> SpecialName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpecialName -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpecialName -> r #

gmapQ :: (forall d. Data d => d -> u) -> SpecialName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecialName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName #

Ord SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Show SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Generic SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep SpecialName :: Type -> Type #

Binary SpecialName Source # 
Instance details

Defined in Idris.Core.Binary

NFData SpecialName Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: SpecialName -> () #

type Rep SpecialName Source # 
Instance details

Defined in Idris.Core.TT

type Rep SpecialName = D1 (MetaData "SpecialName" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((C1 (MetaCons "WhereN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name))) :+: C1 (MetaCons "WithN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name))) :+: (C1 (MetaCons "ImplementationN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Text])) :+: C1 (MetaCons "ParentN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text)))) :+: ((C1 (MetaCons "MethodN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name)) :+: C1 (MetaCons "CaseN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 FC') :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name))) :+: (C1 (MetaCons "ImplementationCtorN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name)) :+: C1 (MetaCons "MetaN" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name)))))

data TC a Source #

Constructors

OK !a 
Error Err 
Instances
Monad TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

(>>=) :: TC a -> (a -> TC b) -> TC b #

(>>) :: TC a -> TC b -> TC b #

return :: a -> TC a #

fail :: String -> TC a #

Functor TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Applicative TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

pure :: a -> TC a #

(<*>) :: TC (a -> b) -> TC a -> TC b #

liftA2 :: (a -> b -> c) -> TC a -> TC b -> TC c #

(*>) :: TC a -> TC b -> TC b #

(<*) :: TC a -> TC b -> TC a #

Alternative TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

empty :: TC a #

(<|>) :: TC a -> TC a -> TC a #

some :: TC a -> TC [a] #

many :: TC a -> TC [a] #

MonadPlus TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

mzero :: TC a #

mplus :: TC a -> TC a -> TC a #

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

Defined in Idris.Core.TT

Methods

(==) :: TC a -> TC a -> Bool #

(/=) :: TC a -> TC a -> Bool #

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

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TC a -> ShowS #

show :: TC a -> String #

showList :: [TC a] -> ShowS #

class TermSize a where Source #

Methods

termsize :: Name -> a -> Int Source #

Instances
TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

TermSize a => TermSize [a] Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> [a] -> Int Source #

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

data TextFormatting Source #

Text formatting output

Instances
Eq TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Ord TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Show TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Generic TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep TextFormatting :: Type -> Type #

NFData TextFormatting Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: TextFormatting -> () #

type Rep TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

type Rep TextFormatting = D1 (MetaData "TextFormatting" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "BoldText" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "ItalicText" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "UnderlineText" PrefixI False) (U1 :: Type -> Type)))

data TT n Source #

Terms in the core language. The type parameter is the type of identifiers used for bindings and explicit named references; usually we use TT Name.

Constructors

P NameType n (TT n)

named references with type (P for Parameter, motivated by McKinna and Pollack's Pure Type Systems Formalized)

V !Int

a resolved de Bruijn-indexed variable

Bind n !(Binder (TT n)) (TT n)

a binding

App (AppStatus n) !(TT n) (TT n)

function, function type, arg

Constant Const

constant

Proj (TT n) !Int

argument projection; runtime only (-1) is a special case for 'subtract one from BI'

Erased

an erased term

Impossible

special case for totality checking

Inferred (TT n)

For building case trees when coverage checkimg only. Marks a term as being inferred by the machine, rather than given by the programmer

TType UExp

the type of types at some level

UType Universe

Uniqueness type universe (disjoint from TType)

Instances
Functor TT Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS #

show :: Err -> String #

showList :: [Err] -> ShowS #

Binary CaseAlt Source # 
Instance details

Defined in Idris.IBC

Methods

put :: CaseAlt -> Put #

get :: Get CaseAlt #

putList :: [CaseAlt] -> Put #

Binary SC Source # 
Instance details

Defined in Idris.IBC

Methods

put :: SC -> Put #

get :: Get SC #

putList :: [SC] -> Put #

NFData Err Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> () #

TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

Eq n => Eq (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: TT n -> TT n -> Bool #

(/=) :: TT n -> TT n -> Bool #

Data n => Data (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TT n -> c (TT n) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TT n) #

toConstr :: TT n -> Constr #

dataTypeOf :: TT n -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TT n)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TT n)) #

gmapT :: (forall b. Data b => b -> b) -> TT n -> TT n #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TT n -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TT n -> r #

gmapQ :: (forall d. Data d => d -> u) -> TT n -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TT n -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TT n -> m (TT n) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TT n -> m (TT n) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TT n -> m (TT n) #

Ord n => Ord (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: TT n -> TT n -> Ordering #

(<) :: TT n -> TT n -> Bool #

(<=) :: TT n -> TT n -> Bool #

(>) :: TT n -> TT n -> Bool #

(>=) :: TT n -> TT n -> Bool #

max :: TT n -> TT n -> TT n #

min :: TT n -> TT n -> TT n #

(Eq n, Show n) => Show (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TT n -> ShowS #

show :: TT n -> String #

showList :: [TT n] -> ShowS #

Generic (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (TT n) :: Type -> Type #

Methods

from :: TT n -> Rep (TT n) x #

to :: Rep (TT n) x -> TT n #

ToJSON t => ToJSON (TT t) Source # 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: TT t -> Value #

toEncoding :: TT t -> Encoding #

toJSONList :: [TT t] -> Value #

toEncodingList :: [TT t] -> Encoding #

Binary (TT Name) Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: TT Name -> Put #

get :: Get (TT Name) #

putList :: [TT Name] -> Put #

NFData n => NFData (TT n) Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: TT n -> () #

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

MonadException m => MonadException (ExceptT Err m) Source # 
Instance details

Defined in Idris.Output

Methods

controlIO :: (RunIO (ExceptT Err m) -> IO (ExceptT Err m a)) -> ExceptT Err m a #

type Rep (TT n) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (TT n) = D1 (MetaData "TT" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((C1 (MetaCons "P" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameType) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT n)))) :+: C1 (MetaCons "V" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int))) :+: (C1 (MetaCons "Bind" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Binder (TT n))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT n)))) :+: (C1 (MetaCons "App" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (AppStatus n)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (TT n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT n)))) :+: C1 (MetaCons "Constant" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Const))))) :+: ((C1 (MetaCons "Proj" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) :+: (C1 (MetaCons "Erased" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Impossible" PrefixI False) (U1 :: Type -> Type))) :+: (C1 (MetaCons "Inferred" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TT n))) :+: (C1 (MetaCons "TType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UExp)) :+: C1 (MetaCons "UType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Universe))))))

type Type = Term Source #

data TypeInfo Source #

Constructors

TI 
Instances
Show TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

Generic TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep TypeInfo :: Type -> Type #

Methods

from :: TypeInfo -> Rep TypeInfo x #

to :: Rep TypeInfo x -> TypeInfo #

Binary TypeInfo Source # 
Instance details

Defined in Idris.IBC

Methods

put :: TypeInfo -> Put #

get :: Get TypeInfo #

putList :: [TypeInfo] -> Put #

NFData TypeInfo Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: TypeInfo -> () #

type Rep TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

data UConstraint Source #

Universe constraints

Constructors

ULT UExp UExp

Strictly less than

ULE UExp UExp

Less than or equal to

Instances
Eq UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Data UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UConstraint -> c UConstraint #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UConstraint #

toConstr :: UConstraint -> Constr #

dataTypeOf :: UConstraint -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UConstraint) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UConstraint) #

gmapT :: (forall b. Data b => b -> b) -> UConstraint -> UConstraint #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UConstraint -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UConstraint -> r #

gmapQ :: (forall d. Data d => d -> u) -> UConstraint -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UConstraint -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint #

Ord UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Show UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Generic UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep UConstraint :: Type -> Type #

Binary UConstraint Source # 
Instance details

Defined in Idris.Core.Binary

NFData UConstraint Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: UConstraint -> () #

type Rep UConstraint Source # 
Instance details

Defined in Idris.Core.TT

type UCs = (Int, [UConstraint]) Source #

data UExp Source #

Universe expressions for universe checking

Constructors

UVar String Int

universe variable, with source file to disambiguate

UVal Int

explicit universe level

Instances
Eq UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

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

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

Data UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UExp -> c UExp #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UExp #

toConstr :: UExp -> Constr #

dataTypeOf :: UExp -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UExp) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UExp) #

gmapT :: (forall b. Data b => b -> b) -> UExp -> UExp #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UExp -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UExp -> r #

gmapQ :: (forall d. Data d => d -> u) -> UExp -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UExp -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UExp -> m UExp #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UExp -> m UExp #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UExp -> m UExp #

Ord UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: UExp -> UExp -> Ordering #

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

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

(>) :: UExp -> UExp -> Bool #

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

max :: UExp -> UExp -> UExp #

min :: UExp -> UExp -> UExp #

Show UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> UExp -> ShowS #

show :: UExp -> String #

showList :: [UExp] -> ShowS #

Generic UExp Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep UExp :: Type -> Type #

Methods

from :: UExp -> Rep UExp x #

to :: Rep UExp x -> UExp #

ToJSON UExp Source # 
Instance details

Defined in IRTS.Portable

Binary UExp Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: UExp -> Put #

get :: Get UExp #

putList :: [UExp] -> Put #

NFData UExp Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: UExp -> () #

type Rep UExp Source # 
Instance details

Defined in Idris.Core.TT

data Universe Source #

Constructors

NullType 
UniqueType 
AllTypes 
Instances
Eq Universe Source # 
Instance details

Defined in Idris.Core.TT

Data Universe Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Universe -> c Universe #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Universe #

toConstr :: Universe -> Constr #

dataTypeOf :: Universe -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Universe) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Universe) #

gmapT :: (forall b. Data b => b -> b) -> Universe -> Universe #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Universe -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Universe -> r #

gmapQ :: (forall d. Data d => d -> u) -> Universe -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Universe -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Universe -> m Universe #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Universe -> m Universe #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Universe -> m Universe #

Ord Universe Source # 
Instance details

Defined in Idris.Core.TT

Show Universe Source # 
Instance details

Defined in Idris.Core.TT

Generic Universe Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Universe :: Type -> Type #

Methods

from :: Universe -> Rep Universe x #

to :: Rep Universe x -> Universe #

Binary Universe Source # 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Universe -> Put #

get :: Get Universe #

putList :: [Universe] -> Put #

NFData Universe Source # 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Universe -> () #

type Rep Universe Source # 
Instance details

Defined in Idris.Core.TT

type Rep Universe = D1 (MetaData "Universe" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "NullType" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "UniqueType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "AllTypes" PrefixI False) (U1 :: Type -> Type)))

addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a Source #

addBinder :: TT n -> TT n Source #

addDef :: Name -> a -> Ctxt a -> Ctxt a Source #

allTTNames :: Eq n => TT n -> [n] Source #

arity :: TT n -> Int Source #

Return the arity of a (normalised) type

bindAll :: [(n, Binder (TT n))] -> TT n -> TT n Source #

Introduce a Bind into the given term for each element of the given list of (name, binder) pairs.

bindingOf Source #

Arguments

:: Name

^ the bound name

-> Bool

^ whether the name is implicit

-> Doc OutputAnnotation 

Pretty-printer helper for the binding site of a name

bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n Source #

Like bindAll, but the Binders are TT terms instead. The first argument is a function to map TT terms to Binders. This function might often be something like Lam, which directly constructs a Binder from a TT term.

constDocs :: Const -> String Source #

Get the docstring for a Const

constIsType :: Const -> Bool Source #

Determines whether the input constant represents a type

discard :: Monad m => m a -> m () Source #

emptyFC :: FC Source #

Empty source location

explicitNames :: TT n -> TT n Source #

Replace all non-free de Bruijn references in the given term with references to the name of their binding.

fc_end :: FC -> (Int, Int) Source #

Give a notion of end location associated with an FC

fc_fname :: FC -> String Source #

Give a notion of filename associated with an FC

fc_start :: FC -> (Int, Int) Source #

Give a notion of start location associated with an FC

fcIn :: FC -> FC -> Bool Source #

Determine whether the first argument is completely contained in the second

fileFC :: String -> FC Source #

Source location with file only

finalise :: Eq n => TT n -> TT n Source #

Replace every non-free reference to the name of a binding in the given term with a de Bruijn index.

fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b) Source #

forget :: TT Name -> Raw Source #

Cast a TT term to a Raw value, discarding universe information and the types of named references and replacing all de Bruijn indices with the corresponding name. It is an error if there are free de Bruijn indices.

freeNames :: Eq n => TT n -> [n] Source #

Returns all names used free in the term

getArgTys :: TT n -> [(n, TT n)] Source #

Return a list of pairs of the names of the outermost Pi-bound variables in the given term, together with their types.

getRetTy :: TT n -> TT n Source #

substRetTy :: TT n -> TT n Source #

As getRetTy but substitutes names for de Bruijn indices

instantiate :: TT n -> TT n -> TT n Source #

Replace the outermost (index 0) de Bruijn variable with the given term

isInjective :: TT n -> Bool Source #

A term is injective iff it is a data constructor, type constructor, constant, the type Type, pi-binding, or an application of an injective term.

lookupCtxt :: Name -> Ctxt a -> [a] Source #

lookupCtxtName :: Name -> Ctxt a -> [(Name, a)] Source #

Look up a name in the context, given an optional namespace. The name (n) may itself have a (partial) namespace given.

Rules for resolution:

  • if an explicit namespace is given, return the names which match it. If none match, return all names.
  • if the name has has explicit namespace given, return the names which match it and ignore the given namespace.
  • otherwise, return all names.

mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b Source #

mkApp :: TT n -> [TT n] -> TT n Source #

Returns a term representing the application of the first argument (a function) to every element of the second argument.

noOccurrence :: Eq n => n -> TT n -> Bool Source #

Returns true if V 0 and bound name n do not occur in the term

occurrences :: Eq n => n -> TT n -> Int Source #

Return number of occurrences of V 0 or bound name i the term

pEraseType :: TT n -> TT n Source #

pmap :: (t -> b) -> (t, t) -> (b, b) Source #

pprintRaw Source #

Arguments

:: [Name]

Bound names, for highlighting

-> Raw

The term to pretty-print

-> Doc OutputAnnotation 

Pretty-print a raw term.

pprintTT Source #

Arguments

:: [Name]

The bound names (for highlighting and de Bruijn indices)

-> TT Name

The term to be printed

-> Doc OutputAnnotation 

Pretty-print a term

psubst :: Eq n => n -> TT n -> TT n -> TT n Source #

pToV :: Eq n => n -> TT n -> TT n Source #

Replace references to the given Name-like id with references to de Bruijn index 0.

pToVs :: Eq n => [n] -> TT n -> TT n Source #

Convert several names. First in the list comes out as V 0

pureTerm :: TT Name -> Bool Source #

Check whether a term has any hole bindings in it - impure if so

showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String Source #

showEnvDbg :: (Show a, Eq a) => [(a, RigCount, Binder (TT a))] -> TT a -> [Char] Source #

sNS :: Name -> [String] -> Name Source #

subst Source #

Arguments

:: Eq n 
=> n

The id to replace

-> TT n

The replacement term

-> TT n

The term to replace in

-> TT n 

As instantiate, but in addition to replacing V 0, replace references to the given Name-like id.

substNames :: Eq n => [(n, TT n)] -> TT n -> TT n Source #

As subst, but takes a list of (name, substitution) pairs instead of a single name and substitution

substTerm Source #

Arguments

:: Eq n 
=> TT n

Old term

-> TT n

New term

-> TT n

template term

-> TT n 

Replaces all terms equal (in the sense of (==)) to the old term with the new term.

substV :: TT n -> TT n -> TT n Source #

As instantiate, but also decrement the indices of all de Bruijn variables remaining in the term, so that there are no more references to the variable that has been substituted.

tcname :: Name -> Bool Source #

Return True if the argument Name should be interpreted as the name of a interface.

termSmallerThan :: Int -> Term -> Bool Source #

Hard-code a heuristic maximum term size, to prevent attempts to serialize or force infinite or just gigantic terms

tfail :: Err -> TC a Source #

toAlist :: Ctxt a -> [(Name, a)] Source #

traceWhen :: Bool -> String -> p -> p Source #

unApply :: TT n -> (TT n, [TT n]) Source #

Deconstruct an application; returns the function and a list of arguments

updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a Source #

vToP :: TT n -> TT n Source #

Replace de Bruijn indices in the given term with explicit references to the names of the bindings they refer to. It is an error if the given term contains free de Bruijn indices.

weakenTm :: Int -> TT n -> TT n Source #

Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

fstEnv :: (a, b, c) -> a Source #

rigEnv :: (a, b, c) -> b Source #

sndEnv :: (a, b, c) -> c Source #

lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n)) Source #

envBinders :: [(a, b1, b2)] -> [(a, b2)] Source #

envZero :: [(a, b, c)] -> [(a, RigCount, c)] Source #