Figure out how to import arithmetic operations in Agda

[swamp-agr]

While the errors from Agda REPL and bot are the same, the scope is different:

• Agda REPL scope:

 :scope
ScopeInfo
  current = agda394558218
  context = []
  modules
    scope
      private
        names
          Prop --> [Agda.Primitive.Prop]
          Set --> [Agda.Primitive.Set]
      imports
        [Agda.Primitive]
    scope agda394558218
      private
        names
          _*_ --> [Agda.Builtin.Nat._*_]
          _+_ --> [Agda.Builtin.Nat._+_]
          _-_ --> [Agda.Builtin.Nat._-_]
          _<_ --> [Agda.Builtin.Nat._<_]
          _==_ --> [Agda.Builtin.Nat._==_]
          Nat --> [Agda.Builtin.Nat.Nat]
          div-helper --> [Agda.Builtin.Nat.div-helper]
          mod-helper --> [Agda.Builtin.Nat.mod-helper]
          suc --> [Agda.Builtin.Nat.Nat.suc]
          zero --> [Agda.Builtin.Nat.Nat.zero]
        modules
          Nat --> [Agda.Builtin.Nat.Nat]
      imports
        [Agda.Builtin.Nat]
    scope Agda.Primitive
      public
        names
          _⊔_ --> [Agda.Primitive._⊔_]
          Level --> [Agda.Primitive.Level]
          Prop --> [Agda.Primitive.Prop]
          SSet --> [Agda.Primitive.SSet]
          SSetω --> [Agda.Primitive.SSetω]
          Set --> [Agda.Primitive.Set]
          Setω --> [Agda.Primitive.Setω]
          lsuc --> [Agda.Primitive.lsuc]
          lzero --> [Agda.Primitive.lzero]
    scope Agda.Builtin.Nat
      public
        names
          _*_ --> [Agda.Builtin.Nat._*_]
          _+_ --> [Agda.Builtin.Nat._+_]
          _-_ --> [Agda.Builtin.Nat._-_]
          _<_ --> [Agda.Builtin.Nat._<_]
          _==_ --> [Agda.Builtin.Nat._==_]
          Nat --> [Agda.Builtin.Nat.Nat]
          div-helper --> [Agda.Builtin.Nat.div-helper]
          mod-helper --> [Agda.Builtin.Nat.mod-helper]
          suc --> [Agda.Builtin.Nat.Nat.suc]
          zero --> [Agda.Builtin.Nat.Nat.zero]
        modules
          Nat --> [Agda.Builtin.Nat.Nat]
    scope Agda.Builtin.Nat.Nat
      public
        names
          suc --> [Agda.Builtin.Nat.Nat.suc]
          zero --> [Agda.Builtin.Nat.Nat.zero]

• Bot scope:

ScopeInfo
  current =
  context = []
  modules
    scope
      private
        names
          Prop --> [Agda.Primitive.Prop]
          Set --> [Agda.Primitive.Set]
      imports
        [Agda.Primitive]
    scope Agda.Primitive
      public
        names
          _⊔_ --> [Agda.Primitive._⊔_]
          Level --> [Agda.Primitive.Level]
          Prop --> [Agda.Primitive.Prop]
          SSet --> [Agda.Primitive.SSet]
          SSetω --> [Agda.Primitive.SSetω]
          Set --> [Agda.Primitive.Set]
          Setω --> [Agda.Primitive.Setω]
          lsuc --> [Agda.Primitive.lsuc]
          lzero --> [Agda.Primitive.lzero]

The idea is to allow bot to keep imports in the current session scope.