diff --git a/NEWS.md b/NEWS.md
index 26a4d4c1..e7b62c9e 100644
--- a/NEWS.md
+++ b/NEWS.md
@@ -5,6 +5,7 @@ ethos 0.1.1 prerelease
 
 - When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options `--no-normalize-dec`, `--no-normalize-hex`, `--binder-fresh`, and `--no-parse-let` now only apply when parsing proofs and reference files.
 - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.
+- Adds support for an attribute `:is_eq` to test whether a defined term is equal to another.
 - Fixed a bug when applying operators with opaque arguments.
 
 ethos 0.1.0
diff --git a/src/attr.cpp b/src/attr.cpp
index be5b59ed..e005add7 100644
--- a/src/attr.cpp
+++ b/src/attr.cpp
@@ -18,6 +18,7 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::VAR: o << "VAR"; break;
     case Attr::IMPLICIT: o << "IMPLICIT"; break;
     case Attr::TYPE: o << "TYPE"; break;
+    case Attr::IS_EQ: o << "IS_EQ"; break;
     case Attr::SORRY: o << "SORRY"; break;
     case Attr::LIST: o << "LIST"; break;
     case Attr::REQUIRES: o << "REQUIRES"; break;
diff --git a/src/attr.h b/src/attr.h
index 39f94a66..99c31f9b 100644
--- a/src/attr.h
+++ b/src/attr.h
@@ -23,7 +23,9 @@ enum class Attr
   VAR,
   IMPLICIT,
   REQUIRES,
+  // inspecting define
   TYPE,
+  IS_EQ,
   // properties of rules
   SORRY,
 
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
index 3d36e936..8266343a 100644
--- a/src/expr_parser.cpp
+++ b/src/expr_parser.cpp
@@ -78,6 +78,7 @@ ExprParser::ExprParser(Lexer& lex, State& state, bool isSignature)
 {
   d_strToAttr[":var"] = Attr::VAR;
   d_strToAttr[":implicit"] = Attr::IMPLICIT;
+  d_strToAttr[":is_eq"] = Attr::IS_EQ;
   d_strToAttr[":type"] = Attr::TYPE;
   d_strToAttr[":list"] = Attr::LIST;
   d_strToAttr[":requires"] = Attr::REQUIRES;
@@ -1165,15 +1166,27 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
         break;
       case Kind::LAMBDA:
       {
-        // only :type is available in define
+        Assert (!e.isNull());
         if (a==Attr::TYPE)
         {
-          Assert (!e.isNull());
           handled = true;
           val = parseExpr();
           // run type checking
           typeCheck(e, val);
         }
+        else if (a==Attr::IS_EQ)
+        {
+          handled = true;
+          val = parseExpr();
+          if (e!=val)
+          {
+            std::stringstream msg;
+            msg << "Terms are not equal:" << std::endl;
+            msg << "Expression: " << e << std::endl;
+            msg << "Target expression: " << val << std::endl;
+            d_lex.parseError(msg.str());
+          }
+        }
       }
         break;
       case Kind::NONE:
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index b81ec019..f334919a 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -126,6 +126,7 @@ set(ethos_test_file_list
     disamb-arith.eo
     opaque-inline.eo
     implicit-then-var.eo
+    is_eq.eo
 )
 
 macro(ethos_test file)
diff --git a/tests/is_eq.eo b/tests/is_eq.eo
new file mode 100644
index 00000000..feea695f
--- /dev/null
+++ b/tests/is_eq.eo
@@ -0,0 +1,3 @@
+
+(define test () (eo::add 1 1) :is_eq 2)
+