 removeForced :: MonadTCM m => CompiledClauses > Type > Compile m CompiledClauses
 constrType :: MonadTCM m => QName > Compile m Type
 dataParameters :: MonadTCM m => QName > Compile m Nat
 isIn :: MonadTCM m => Nat > CompiledClauses > Compile m Bool
 isInCase :: MonadTCM m => Nat > (Nat, Case CompiledClauses) > Compile m Bool
 isInTerm :: Nat > Term > Bool
 insertTele :: MonadTCM m => Int > Maybe Type > Term > Telescope > Compile m (Telescope, (Type, Type))
 unifyI :: MonadTCM m => Telescope > [Nat] > Type > Args > Args > Compile m [Maybe Term]
 remForced :: MonadTCM m => CompiledClauses > Telescope > Compile m CompiledClauses
 data FoldState = FoldState {}
 foldM' :: Monad m => a > [b] > (a > b > m a) > m a
 lift2 :: (MonadTrans t, Monad (t1 m), MonadTrans t1, Monad m) => m a > t (t1 m) a
 modifyM :: MonadState a m => (a > m a) > m ()
 replaceForced :: MonadTCM m => (Nat, Telescope) > [Nat] > (CompiledClauses, [Maybe Term]) > Compile m CompiledClauses
 raiseFromCC :: Nat > Nat > CompiledClauses > CompiledClauses
 substCC :: MonadTCM m => [Nat] > CompiledClauses > StateT FoldState (Compile m) CompiledClauses
 substCCBody :: Nat > Term > CompiledClauses > CompiledClauses
 substsCCBody :: [Term] > CompiledClauses > CompiledClauses
 findPosition :: Nat > [Maybe Term] > (Nat, Term)
Documentation
removeForced :: MonadTCM m => CompiledClauses > Type > Compile m CompiledClausesSource
Replace the uses of forced variables in a CompiledClauses with the function arguments that they correspond to. Note that this works on CompiledClauses where the term's variable indexes have been reversed, which means that the case variables match the variables in the term.
constrType :: MonadTCM m => QName > Compile m TypeSource
Returns the type of a constructor given its name
dataParameters :: MonadTCM m => QName > Compile m NatSource
Returns how many parameters a datatype has
isIn :: MonadTCM m => Nat > CompiledClauses > Compile m BoolSource
Is variable n used in a CompiledClause?
:: MonadTCM m  
=> Int  ABS 
> Maybe Type  If Just, it is the type to insert patterns from is nothing if we only want to delete a binding. 
> Term  Term to replace at pos 
> Telescope  The telescope 
> Compile m (Telescope, (Type, Type))  Returns (resulting telescope, the type at pos in tele, the return type of the inserted type). 
insertTele i xs t tele
tpos
tele := Gamma ; (i : T as) ; Delta
n := parameters T
xs' := xs apply
(take n as)
becomes
tpos
( Gamma ; xs' ; Delta[i := t] note that Delta still reference Gamma correctly
, T as ^ (size xs')
)
we raise the type since we have added xs' new bindings before Gamma, and as can only bind to Gamma.
:: MonadTCM m  
=> CompiledClauses  Remove cases on forced variables in this 
> Telescope  The current context we are in 
> Compile m CompiledClauses 
Remove forced variables cased on in the current toplevel case in the CompiledClauses
FoldState  

lift2 :: (MonadTrans t, Monad (t1 m), MonadTrans t1, Monad m) => m a > t (t1 m) aSource
modifyM :: MonadState a m => (a > m a) > m ()Source
replaceForced :: MonadTCM m => (Nat, Telescope) > [Nat] > (CompiledClauses, [Maybe Term]) > Compile m CompiledClausesSource
replaceForced (tpos, tele) forcedVars (cc, unification) For each forceVar dig out the corresponding case and continue to remForced.
raiseFromCC :: Nat > Nat > CompiledClauses > CompiledClausesSource
substCC :: MonadTCM m => [Nat] > CompiledClauses > StateT FoldState (Compile m) CompiledClausesSource
Substitute with the Substitution, this will adjust with the new bindings in the CompiledClauses
substCCBody :: Nat > Term > CompiledClauses > CompiledClausesSource
Substitute variable n for term t in the body of cc
substsCCBody :: [Term] > CompiledClauses > CompiledClausesSource
Perform a substitution in the body of cc