Idris2Doc : TTImp.ProcessRecord

TTImp.ProcessRecord

(source)

Definitions

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