4 files changed, 2 insertions, 8 deletions
diff --git a/src/Term/Compile.idr b/src/Term/Compile.idr
index dd423ae..ba409a8 100644
--- a/src/Term/Compile.idr
+++ b/src/Term/Compile.idr
@@ -35,10 +35,6 @@ lambda = "lambda"
 lit : Nat -> Doc ann
 lit = pretty
 
-compileArb : Ty -> Doc ann
-compileArb N = pretty 0
-compileArb (ty ~> ty') = parens $ group $ "const" <+> softline <+> compileArb ty'
-
 compileOp : Operator tys ty -> Doc ann
 compileOp (Lit n) = lit n
 compileOp Suc = "1+"
@@ -52,7 +48,6 @@ compileOp (Inl _ _) = identity_
 compileOp (Inr _ _) = identity_
 compileOp (Prl _ _) = identity_
 compileOp (Prr _ _) = identity_
-compileOp (Arb ty) = compileArb ty
 
 parameters (names : Stream String)
   compileFullTerm : (len : Len ctx) => FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc ann
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index 043d478..1b62dc3 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -156,7 +156,6 @@ prettyOp (Inl _ _) = keyword "inl"
 prettyOp (Inr _ _) = keyword "inr"
 prettyOp (Prl _ _) = keyword "prl"
 prettyOp (Prr _ _) = keyword "prr"
-prettyOp (Arb _) = keyword "arb"
 
 parameters (names : Stream String)
   prettyTerm' : (len : Len ctx) => Prec -> Term ty ctx -> Doc Syntax
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index c31a9e6..eb1c9c5 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -70,7 +70,6 @@ opSem (Inl ty1 ty2) = inl ty1 ty2
 opSem (Inr ty1 ty2) = swap ty2 ty1 . inl ty2 ty1
 opSem (Prl ty1 ty2) = prl ty1 ty2
 opSem (Prr ty1 ty2) = prl ty2 ty1 . swap ty1 ty2
-opSem (Arb ty) = arb ty
 
 %inline
 sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index d403440..5a134a2 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -43,7 +43,8 @@ t `mod` u = App (App (Op Mod) t) u
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb = Op (Arb ty)
+Arb {ty = N} = Op (Lit 0)
+Arb {ty = ty ~> ty'} = Const Arb
 
 export
 inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx