add description of #check_failure

leanprover-community · Apr 20, 2024 · 06f48bf · 06f48bf
1 parent cc108fa
commit 06f48bf
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean
@@ -158,6 +158,8 @@ it just means that the Lean parser can understand it:
 -- elaboration function for 'termMyTerm' has not been implemented
 --   MyTerm
 
+/-! Note: `#check_failure` command allows incorrectly typed terms to be indicated without error. -/
+
 /-!
 Implementing this so-called "elaboration function", which will actually
 give meaning to this syntax in terms of Lean's fundamental `Expr` type,