Lower case

leanprover · Jul 23, 2024 · ed7d26e · ed7d26e
1 parent 04f06ef
commit ed7d26e
Show file tree

Hide file tree

Showing 10 changed files with 15 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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