Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Auto.Typecheck
Documentation
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)Source
getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)Source
constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)Source
unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)Source
unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)Source
traversePi :: Int -> ICExp o -> EE (MyMB (HNExp o) o)Source
tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)Source
type HNNBlks o = [HNExp o]Source
hnn :: ICExp o -> EE (MyMB (HNExp o) o)Source
hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)Source
hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)Source
hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)Source
hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)Source
data HNRes o Source
Constructors
HNDone (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
HNMeta (ICExp o) (ICArgList o) [Maybe (UId o)]
hnc :: Bool -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)Source
hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)Source
getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)Source
getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)Source
data PEval o Source
Constructors
PENo (ICExp o)
PEConApp (ICExp o) (ConstRef o) [PEval o]
iotastep :: Bool -> HNExp o -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)Source
noiotastep :: HNExp o -> EE (MyPB o)Source
noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)Source
data CMode o Source
Constructors
CMRigid (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
forall b . Refinable b (RefInfo o) => CMFlex (MM b (RefInfo o)) (CMFlex o)
data CMFlex o Source
Constructors
CMFFlex (ICExp o) (ICArgList o) [Maybe (UId o)]
CMFSemi (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
CMFBlocked (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
comp' :: forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)Source
checkeliminand :: MExp o -> EE (MyPB o)Source
iotapossmeta :: ICExp o -> ICArgList o -> EE BoolSource
meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))Source
calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)Source
pickid :: MId -> MId -> MIdSource
tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)Source
Produced by Haddock version 2.6.1