diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index f3388ba9..075b3145 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -193,7 +193,7 @@ function parse_model_param(e)
   model_type = @match paramdecl begin
     Expr(:vect, Expr(:(::), :model, model_type)) => model_type
     nothing => nothing
-    _ => error("invalid syntax for declaring model type: $model")
+    _ => error("invalid syntax for declaring model type: $paramdecl")
   end
 
   (model_type, whereparams)
diff --git a/src/stdlib/models/Arithmetic.jl b/src/stdlib/models/Arithmetic.jl
new file mode 100644
index 00000000..fd29e5e8
--- /dev/null
+++ b/src/stdlib/models/Arithmetic.jl
@@ -0,0 +1,16 @@
+module Arithmetic 
+
+export IntNatPlus
+
+using ....Models
+using ...StdTheories
+
+struct IntNatPlus <: Model{Tuple{Int}} end
+
+@instance ThNatPlus{Int} [model::IntNatPlus] begin
+  Z() = 0
+  S(n::Int) = n + 1
+  +(x::Int, y::Int) = x + y
+end
+
+end # module 
diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl
index 328c7fe6..569fb3ed 100644
--- a/src/stdlib/models/module.jl
+++ b/src/stdlib/models/module.jl
@@ -3,6 +3,7 @@ module StdModels
 using Reexport
 
 include("FinSets.jl")
+include("Arithmetic.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Op.jl")
@@ -10,6 +11,7 @@ include("Nothings.jl")
 include("GATs.jl")
 
 @reexport using .FinSets
+@reexport using .Arithmetic
 @reexport using .FinMatrices
 @reexport using .SliceCategories
 @reexport using .Op
diff --git a/src/stdlib/theories/Naturals.jl b/src/stdlib/theories/Naturals.jl
index b226c129..aac38948 100644
--- a/src/stdlib/theories/Naturals.jl
+++ b/src/stdlib/theories/Naturals.jl
@@ -12,6 +12,7 @@ using ....Syntax
 end
 
 @theory ThNatPlus <: ThNat begin
+  import Base: +
   ((x::ℕ) + (y::ℕ))::ℕ
   (n + S(m) == S(n+m) :: ℕ) ⊣ [n::ℕ,m::ℕ]
 end
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 25450d59..9cb73d4e 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -757,7 +757,7 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{JudgmentBinding})
       (name, arglist) = @match head begin
         Expr(:call, name, args...) => (name, args)
         name::Symbol => (name, [])
-        _ => error("failed to parse head of term constructor $call")
+        _ => error("failed to parse head of term constructor $head")
       end
       args = parsetypescope(c′, arglist; bound=Set(nameof.(localcontext)))
       @match type_expr begin
@@ -795,25 +795,29 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{GATSegment})
   c′ = AppendScope(c, seg)
   linenumber = nothing
   for line in e.args
-    @match line begin
-      l::LineNumberNode => (linenumber = l)
-      Expr(:macrocall, var"@op", _, aliasexpr) => begin
+    @switch line begin
+      @case l::LineNumberNode
+        (linenumber = l)
+      @case Expr(:macrocall, var"@op", _, aliasexpr)
         lines = @match aliasexpr begin
           Expr(:block, lines...) => lines
           _ => [aliasexpr]
         end
         for line in lines
-          @match line begin
-            _::LineNumberNode => nothing
-            :($alias := $name) => Scopes.unsafe_addalias!(seg, name, alias)
-            _ => error("could not match @op line $line")
+          @switch line begin
+            @case (_::LineNumberNode) 
+              nothing
+            @case :($alias := $name) 
+              Scopes.unsafe_addalias!(seg, name, alias)
+            @case _
+              error("could not match @op line $line")
           end
         end
-      end
-      _ => begin
+      @case Expr(:import, Expr(:(:), Expr(:(.), mod), imports))
+        nothing
+      @case _ 
         binding = setline(fromexpr(c′, line, JudgmentBinding), linenumber)
         Scopes.unsafe_pushbinding!(seg, binding)
-      end
     end
   end
   seg
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 22125d65..361a385b 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -53,13 +53,23 @@ macro theory(head, body)
   end
 
   newsegment = fromexpr(parent, body, GATSegment)
+  importlines = Expr[]
+  for line in body.args
+    @switch line begin 
+      @case Expr(:import, Expr(:(:), Expr(:., mod), imports)) 
+        push!(importlines, line)
+      @case _ 
+        nothing 
+    end 
+  end
+
 
   theory = GAT(name, parent, newsegment)
 
   modulelines = Any[]
 
   push!(modulelines, :(export $(allnames(theory; aliases=true)...)))
-
+  append!(modulelines, importlines)
   if !isnothing(parentname)
     push!(modulelines, Expr(:using, Expr(:(.), :(.), :(.), parentname)))
   end
diff --git a/test/stdlib/models/Arithmetic.jl b/test/stdlib/models/Arithmetic.jl
new file mode 100644
index 00000000..81d3d55d
--- /dev/null
+++ b/test/stdlib/models/Arithmetic.jl
@@ -0,0 +1,13 @@
+module TestArithmetic 
+
+using GATlab
+using Test
+
+using .ThNatPlus
+
+@withmodel IntNatPlus() (ℕ, Z, S, +) begin
+  @test S(S(Z())) + Z() == 2
+end
+
+
+end # module 
diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl
index 6555e913..7893f362 100644
--- a/test/stdlib/models/tests.jl
+++ b/test/stdlib/models/tests.jl
@@ -1,6 +1,7 @@
 module TestStdModels
 
 include("FinSets.jl")
+include("Arithmetic.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Op.jl")