From 51d1cc61d7d288e9dbf4111b7c26ecaaa09b055c Mon Sep 17 00:00:00 2001 From: Andrii Kurdiumov Date: Sat, 23 Nov 2024 13:56:31 +0600 Subject: [PATCH] fix: remove obsolete sentence in doc-string (#6185) Even if this sentence is technically true, it do not add anything to the explanation of typechecker and code. --- doc/examples/tc.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/doc/examples/tc.lean b/doc/examples/tc.lean index c6c3cd21a7..2b8252f744 100644 --- a/doc/examples/tc.lean +++ b/doc/examples/tc.lean @@ -82,9 +82,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un /-! Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold. The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`. -The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to rename "inaccessible" variables. -We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced -by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes +The proof is by induction on `e` and case analysis. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes the cases corresponding to the constructors `Expr.nat` and `Expr.bool`. -/ theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by