Safe Haskell | Safe-Inferred |
---|
Agda.Auto.Syntax
Documentation
data EqReasoningConsts o
data EqReasoningState
Instances
data RefInfo o
Constructors
RIEnv | |
Fields
| |
RIMainInfo Nat (HNExp o) Bool | |
forall a . RIUnifInfo [CAction o] (HNExp o) | |
RICopyInfo (ICExp o) | |
RIIotaStep Bool | |
RIInferredTypeUnknown | |
RINotConstructor | |
RIUsedVars [UId o] [Elr o] | |
RIPickSubsvar | |
RIEqRState EqReasoningState | |
RICheckElim Bool | |
RICheckProjIndex [ConstRef o] |
data DeclCont o
data Sort
Constructors
Set Nat | |
UnknownSort | |
Type |
data Exp o
data ArgList o
data HNExp o
data HNArgList o
data Clos a o
data TrBr a o
detecteliminand :: [Clause o] -> Maybe Nat
detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
categorizedecl :: ConstRef o -> IO ()
metaliseokh :: MExp o -> IO (MExp o)
addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
weakarglist :: Nat -> ICArgList o -> ICArgList o