TTImp.ProcessData

Definitions

findNewtype : Ref Ctxt Defs => List Constructor -> Core ()

Visibility: export

processData : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => List ElabOpt -> NestedNames vars -> Env Term vars -> FC -> WithDefault Visibility Private -> Maybe TotalReq -> ImpData -> Core ()

Visibility: export