TTImp.ProcessBuiltin

Checking a %builtin pragma is correct.

Definitions

processBuiltin : Ref Ctxt Defs => NestedNames vars -> Env Term vars -> FC -> BuiltinType -> Name -> Core ()

  Check a `%builtin` pragma is correct.

Visibility: export