diff --git a/tests/lean/1301.lean b/tests/lean/1301.lean
new file mode 100644
index 0000000000..ba57c1a094
--- /dev/null
+++ b/tests/lean/1301.lean
@@ -0,0 +1,10 @@
+syntax "tac" : tactic
+theorem a : True := by tac
+#check a -- should be declared
+
+theorem a' : True ∧ True := ⟨by tac, by tac⟩
+#check a' -- should be declared
+
+syntax "term" : term
+def b (n : Nat) : Nat := term
+#print b -- should be declared
diff --git a/tests/lean/1301.lean.expected.out b/tests/lean/1301.lean.expected.out
new file mode 100644
index 0000000000..964b6e3b2d
--- /dev/null
+++ b/tests/lean/1301.lean.expected.out
@@ -0,0 +1,8 @@
+1301.lean:2:23-2:26: error: tactic 'tacticTac' has not been implemented
+a : True
+1301.lean:5:32-5:35: error: tactic 'tacticTac' has not been implemented
+a' : True ∧ True
+1301.lean:9:25-9:29: error: elaboration function for 'termTerm' has not been implemented
+  term
+def b : Nat → Nat :=
+sorryAx (Nat → Nat) true