From ed7d26e00c386db44fad6adea9371ea8e238c441 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 23 Jul 2024 12:03:02 +0200 Subject: [PATCH] Lower case --- src/Lean/Elab/BuiltinCommand.lean | 2 +- tests/lean/277a.lean.expected.out | 2 +- tests/lean/277b.lean.expected.out | 2 +- tests/lean/440.lean.expected.out | 2 +- tests/lean/evalSorry.lean.expected.out | 4 ++-- tests/lean/phashmap_inst_coherence.lean.expected.out | 2 +- tests/lean/prvCtor.lean.expected.out | 2 +- tests/lean/run/1697.lean | 4 ++-- tests/lean/run/3713.lean | 4 ++-- tests/lean/scientific.lean.expected.out | 6 +++--- 10 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index bff8ff2f0668..8b18ec1fdb44 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -363,7 +363,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Uni unless bang do let axioms ← collectAxioms declName if axioms.contains ``sorryAx then - throwError ("Cannot evaluate expression that depends on the `sorry` axiom.\nUse `#eval!` to " ++ + throwError ("cannot evaluate expression that depends on the `sorry` axiom.\nUse `#eval!` to " ++ "evaluate nevertheless (which may cause lean to crash).") -- Elaborate `term` let elabEvalTerm : TermElabM Expr := do diff --git a/tests/lean/277a.lean.expected.out b/tests/lean/277a.lean.expected.out index ef5e66e59c83..2b26de9bdddc 100644 --- a/tests/lean/277a.lean.expected.out +++ b/tests/lean/277a.lean.expected.out @@ -1,3 +1,3 @@ 277a.lean:4:7-4:15: error: unknown identifier 'nonexistant' -277a.lean:4:0-4:25: error: Cannot evaluate expression that depends on the `sorry` axiom. +277a.lean:4:0-4:25: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/277b.lean.expected.out b/tests/lean/277b.lean.expected.out index 3b9db5a826bc..34b17b676d62 100644 --- a/tests/lean/277b.lean.expected.out +++ b/tests/lean/277b.lean.expected.out @@ -1,4 +1,4 @@ 277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor List Point -277b.lean:8:0-8:16: error: Cannot evaluate expression that depends on the `sorry` axiom. +277b.lean:8:0-8:16: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/440.lean.expected.out b/tests/lean/440.lean.expected.out index 5216fc0af175..720305265ce3 100644 --- a/tests/lean/440.lean.expected.out +++ b/tests/lean/440.lean.expected.out @@ -6,5 +6,5 @@ context: x : Nat ⊢ Nat f (x : Nat) : Nat -440.lean:11:0-11:9: error: Cannot evaluate expression that depends on the `sorry` axiom. +440.lean:11:0-11:9: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out index 40a5689ec2d6..ecd7abad9752 100644 --- a/tests/lean/evalSorry.lean.expected.out +++ b/tests/lean/evalSorry.lean.expected.out @@ -7,7 +7,7 @@ has type String : Type but is expected to have type Nat : Type -evalSorry.lean:7:0-7:15: error: Cannot evaluate expression that depends on the `sorry` axiom. +evalSorry.lean:7:0-7:15: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -evalSorry.lean:11:0-11:15: error: Cannot evaluate expression that depends on the `sorry` axiom. +evalSorry.lean:11:0-11:15: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index 581f37a4a01d..4f213ccb44d3 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/tests/lean/phashmap_inst_coherence.lean.expected.out @@ -6,5 +6,5 @@ has type @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type but is expected to have type @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type -phashmap_inst_coherence.lean:12:0-12:56: error: Cannot evaluate expression that depends on the `sorry` axiom. +phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out index 30e61d7e300e..a1de1f6b0f4d 100644 --- a/tests/lean/prvCtor.lean.expected.out +++ b/tests/lean/prvCtor.lean.expected.out @@ -1,7 +1,7 @@ a : Nat prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private -prvCtor.lean:23:0-25:61: error: Cannot evaluate expression that depends on the `sorry` axiom. +prvCtor.lean:23:0-25:61: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). prvCtor.lean:27:7-27:8: error: unknown identifier 'a' prvCtor.lean:29:25-29:27: error: overloaded, errors diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index b71e274e8e32..6e865e6f45ba 100644 --- a/tests/lean/run/1697.lean +++ b/tests/lean/run/1697.lean @@ -4,7 +4,7 @@ error: tactic 'decide' proved that the proposition False is false --- -error: Cannot evaluate expression that depends on the `sorry` axiom. +error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in @@ -13,7 +13,7 @@ Use `#eval!` to evaluate nevertheless (which may cause lean to crash). /-- warning: declaration uses 'sorry' --- -error: Cannot evaluate expression that depends on the `sorry` axiom. +error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in diff --git a/tests/lean/run/3713.lean b/tests/lean/run/3713.lean index 7cc6b04b874d..2a3007324936 100644 --- a/tests/lean/run/3713.lean +++ b/tests/lean/run/3713.lean @@ -8,7 +8,7 @@ def somethingBad : MetaM Nat := do /-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression --- -error: Cannot evaluate expression that depends on the `sorry` axiom. +error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in @@ -21,7 +21,7 @@ def foo : MetaM Bool := /-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression --- -error: Cannot evaluate expression that depends on the `sorry` axiom. +error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out index 9cdbaecf9865..4c3f8880e8b9 100644 --- a/tests/lean/scientific.lean.expected.out +++ b/tests/lean/scientific.lean.expected.out @@ -15,7 +15,7 @@ scientific.lean:15:7-15:12: error: unexpected token; expected command scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`) scientific.lean:16:7-16:16: error: unexpected token; expected command scientific.lean:19:6-19:7: error: unknown identifier 'e' -scientific.lean:19:0-19:9: error: Cannot evaluate expression that depends on the `sorry` axiom. +scientific.lean:19:0-19:9: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). scientific.lean:20:9: error: missing exponent digits in scientific literal scientific.lean:21:9: error: missing exponent digits in scientific literal @@ -25,9 +25,9 @@ scientific.lean:24:9: error: missing exponent digits in scientific literal scientific.lean:25:9: error: missing exponent digits in scientific literal scientific.lean:26:6-26:8: error: invalid dotted identifier notation, unknown identifier `Nat.E` from expected type Nat -scientific.lean:26:0-26:11: error: Cannot evaluate expression that depends on the `sorry` axiom. +scientific.lean:26:0-26:11: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). scientific.lean:27:7-27:9: error: unknown identifier 'E3' -scientific.lean:27:0-27:9: error: Cannot evaluate expression that depends on the `sorry` axiom. +scientific.lean:27:0-27:9: error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). scientific.lean:28:7: error: missing exponent digits in scientific literal