Merge pull request #3322 from YDX-2147483647/lean

Update Lean.sublime-syntax from Lean 3 to Lean 4

.gitmodules

@@ -196,7 +196,7 @@
 	branch = bat-source
 [submodule "assets/syntaxes/02_Extra/Lean"]
 	path = assets/syntaxes/02_Extra/Lean
-	url = https://github.com/leanprover/vscode-lean.git
+	url = https://github.com/leanprover/vscode-lean4.git
 [submodule "assets/syntaxes/02_Extra/Zig"]
 	path = assets/syntaxes/02_Extra/Zig
 	url = https://github.com/ziglang/sublime-zig-language.git

CHANGELOG.md

@@ -41,6 +41,7 @@
 - Map `.mill` files to Scala syntax for Mill build tool configuration files #3311 (@krikera)
 - Add syntax highlighting for VHDL, see #3337 (@JerryImMouse)
 - Add syntax mapping for certbot certificate configuration #3338 (@cyqsimon)
+- Update Lean syntax from Lean 3 to Lean 4 #3322 (@YDX-2147483647)
 
 ## Themes
 

assets/syntaxes/02_Extra/Lean.sublime-syntax

@@ -1,125 +1,130 @@
 %YAML 1.2
 ---
-# http://www.sublimetext.com/docs/3/syntax.html
+# http://www.sublimetext.com/docs/syntax.html
-name: Lean
+name: Lean 4
 file_extensions:
   - lean
-scope: source.lean
+scope: source.lean4
 contexts:
   main:
     - include: comments
-    - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\b\s+(\{[^}]*\})?'
+    - match: \b(Prop|Type|Sort)\b
+      scope: storage.type.lean4
+    - match: '\battribute\b\s*\[[^\]]*\]'
+      scope: storage.modifier.lean4
+    - match: '@\[[^\]]*\]'
+      scope: storage.modifier.lean4
+    - match: \b(?<!\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\.)\b
+      scope: storage.modifier.lean4
+    - match: \b(sorry|admit|stop)\b
+      scope: invalid.illegal.lean4
+    - match: '#(print|eval|reduce|check|check_failure)\b'
+      scope: keyword.other.lean4
+    - match: \bderiving\s+instance\b
+      scope: keyword.other.command.lean4
+    - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\b\s+(\{[^}]*\})?'
       captures:
-        1: keyword.other.definitioncommand.lean
+        1: keyword.other.definitioncommand.lean4
       push:
-        - meta_scope: meta.definitioncommand.lean
+        - meta_scope: meta.definitioncommand.lean4
-        - match: '(?=\bwith\b|\bextends\b|[:\|\(\[\{⦃<>])'
+        - match: '(?=\bwith\b|\bextends\b|\bwhere\b|[:\|\(\[\{⦃<>])'
           pop: true
         - include: comments
         - include: definitionName
-        - match: ","
+        - match: ','
-    - match: \b(Prop|Type|Sort)\b
+    - match: \b(?<!\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\.)\b
-      scope: storage.type.lean
+      scope: keyword.other.lean4
-    - match: '\battribute\b\s*\[[^\]]*\]'
-      scope: storage.modifier.lean
-    - match: '@\[[^\]]*\]'
-      scope: storage.modifier.lean
-    - match: \b(?<!\.)(private|meta|mutual|protected|noncomputable)\b
-      scope: keyword.control.definition.modifier.lean
-    - match: \b(sorry)\b
-      scope: invalid.illegal.lean
-    - match: '#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b'
-      scope: keyword.other.command.lean
-    - match: '#(print|eval|reduce|check|help|exit|find|where)\b'
-      scope: keyword.other.command.lean
-    - match: \b(?<!\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\.)\b
-      scope: keyword.other.lean
-    - match: \b(?<!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\.)\b
-      scope: keyword.other.lean
     - match: «
       push:
-        - meta_content_scope: entity.name.lean
+        - meta_content_scope: entity.name.lean4
         - match: »
           pop: true
-    - match: \b(?<!\.)(if|then|else)\b
+    - match: (s!)"
-      scope: keyword.control.lean
-    - match: '"'
       captures:
-        0: punctuation.definition.string.begin.lean
+        1: keyword.other.lean4
       push:
-        - meta_scope: string.quoted.double.lean
+        - meta_scope: string.interpolated.lean4
         - match: '"'
-          captures:
-            0: punctuation.definition.string.end.lean
           pop: true
-        - match: '\\[\\"nt'']'
+        - match: '(\{)'
-          scope: constant.character.escape.lean
+          captures:
+            1: keyword.other.lean4
+          push:
+            - match: '(\})'
+              captures:
+                1: keyword.other.lean4
+              pop: true
+            - include: main
+        - match: '\\[\\"ntr'']'
+          scope: constant.character.escape.lean4
         - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
-          scope: constant.character.escape.lean
+          scope: constant.character.escape.lean4
         - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
-          scope: constant.character.escape.lean
+          scope: constant.character.escape.lean4
+    - match: '"'
+      push:
+        - meta_scope: string.quoted.double.lean4
+        - match: '"'
+          pop: true
+        - match: '\\[\\"ntr'']'
+          scope: constant.character.escape.lean4
+        - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
+          scope: constant.character.escape.lean4
+        - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
+          scope: constant.character.escape.lean4
+    - match: \b(true|false)\b
+      scope: constant.language.lean4
     - match: '''[^\\'']'''
-      scope: string.quoted.single.lean
+      scope: string.quoted.single.lean4
-    - match: '''(\\(x..|u....|.))'''
+    - match: '''(\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'''
-      scope: string.quoted.single.lean
+      scope: string.quoted.single.lean4
       captures:
-        1: constant.character.escape.lean
+        1: constant.character.escape.lean4
     - match: '`+[^\[(]\S+'
-      scope: entity.name.lean
+      scope: entity.name.lean4
-    - match: '\b([0-9]+|0([xX][0-9a-fA-F]+))\b'
+    - match: '\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?)\b'
-      scope: constant.numeric.lean
+      scope: constant.numeric.lean4
   blockComment:
     - match: /-
       push:
-        - meta_scope: comment.block.lean
+        - meta_scope: comment.block.lean4
-        - match: "-/"
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
         - include: blockComment
   comments:
     - include: dashComment
     - include: docComment
-    - include: stringBlock
     - include: modDocComment
     - include: blockComment
   dashComment:
-    - match: (--)
+    - match: '--'
-      captures:
-        0: punctuation.definition.comment.lean
       push:
-        - meta_scope: comment.line.double-dash.lean
+        - meta_scope: comment.line.double-dash.lean4
         - match: $
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
   definitionName:
     - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*'
-      scope: entity.name.function.lean
+      scope: entity.name.function.lean4
     - match: «
       push:
-        - meta_content_scope: entity.name.function.lean
+        - meta_content_scope: entity.name.function.lean4
         - match: »
           pop: true
   docComment:
     - match: /--
       push:
-        - meta_scope: comment.block.documentation.lean
+        - meta_scope: comment.block.documentation.lean4
-        - match: "-/"
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
         - include: blockComment
   modDocComment:
     - match: /-!
       push:
-        - meta_scope: comment.block.documentation.lean
+        - meta_scope: comment.block.documentation.lean4
-        - match: "-/"
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
-        - include: blockComment
-  stringBlock:
-    - match: /-"
-      push:
-        - meta_scope: comment.block.string.lean
-        - match: '"-/'
-          pop: true
-        - include: scope:source.lean.markdown
         - include: blockComment

doc/assets.md

@@ -26,7 +26,7 @@ in the `.sublime-syntax` format.
 4. Re-compile `bat`. At compilation time, the `syntaxes.bin` file will be stored inside the
    `bat` binary.
 
-5. Use `bat --list-languages` to check if the new languages are available. You may want to do something like `export PATH="`pwd`/target/debug:$PATH"` to ensure the locally compiled version is the one being used.
+5. Use `bat --list-languages` to check if the new languages are available. You may want to do something like ``export PATH="`pwd`/target/debug:$PATH"`` to ensure the locally compiled version is the one being used.
 
 6. Add a syntax test for the new language. See [below](#Syntax-tests) for details.
 
@@ -102,4 +102,4 @@ The following files have been manually modified after converting from a `.tmLang
    https://github.com/seanjames777/SML-Language-Definition/blob/master/sml.tmLanguage
 * `Cabal.sublime_syntax` has been added manually from
   https://github.com/SublimeHaskell/SublimeHaskell/ - we don't want to include the whole submodule because it includes other syntaxes ("Haskell improved") as well.
-* `Lean.sublime-syntax` has been added manually from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json via conversion.
+* `Lean.sublime-syntax` has been added manually from https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json via conversion.

src/assets/build_assets/acknowledgements.rs

@@ -95,6 +95,9 @@ fn include_license_in_acknowledgments(license_text: &str) -> bool {
         // Apache 2.0
         "Apache License Version 2.0, January 2004 http://www.apache.org/licenses/",
         "Licensed under the Apache License, Version 2.0 (the \"License\");",
+
+        // CC BY 4.0
+        "Creative Commons Attribution 4.0 International Public License",
     ];
 
     license_contains_marker(license_text, &markers)

tests/syntax-tests/highlighted/Lean/test.lean

@@ -1,67 +1,82 @@
-import data.matrix.notation
+import MIL.Common
-import data.vector2
+import Mathlib.Topology.Instances.Real.Defs
 
-/-!
+open Set Filter Topology
 
-Helpers that don't currently fit elsewhere...
+variable {α : Type*}
+variable (s t : Set ℕ)
+variable (ssubt : s ⊆ t)
+variable {α : Type*} (s : Set (Set α))
+-- Apostrophes are allowed in variable names
+variable (f'_x x' : ℕ)
+variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)
 
--/
+-- In the next example we could use `tauto` in each proof instead of knowing the lemmas
+example {α : Type*} (s : Set α) : Filter α :=
+  { sets := { t | s ⊆ t }
+    univ_sets := subset_univ s
+    sets_of_superset := fun hU hUV ↦ Subset.trans hU hUV
+    inter_sets := fun hU hV ↦ subset_inter hU hV }
 
-lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
-  p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
-
--- For `playfield`s, the piece type and/or piece index type.
-variables (X : Type*)
-variables [has_repr X]
 
 namespace chess.utils
 
 section repr
 
-/--
+@[class] structure One₂ (α : Type) where
-An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
+  /-- The element one -/
-for `option`, and rather, output just the value in the `some` and a custom provided
+  one : α
-`string` for `none`.
--/
-structure option_wrapper :=
-(val : option X)
-(none_s : string)
 
-instance wrapped_option_repr : has_repr (option_wrapper X) :=
+structure StandardTwoSimplex where
-⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
+  x : ℝ
+  y : ℝ
+  z : ℝ
+  x_nonneg : 0 ≤ x
+  y_nonneg : 0 ≤ y
+  z_nonneg : 0 ≤ z
+  sum_eq : x + y + z = 1
 
-variables {X}
+#check Pi.ringHom
-/--
+#check ker_Pi_Quotient_mk
-Construct an `option_wrapper` term from a provided `option X` and the `string`
+#eval 1 + 1
-that will override the `has_repr.repr` for `none`.
--/
-def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
 
--- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
+/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
-variables {m' n' : ℕ}
+  Remainder Theorem. -/
+def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
+  Ideal.Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Ideal.Quotient.mk (I i))
+    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])
 
-/--
+lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
-For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
+    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
-the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
+  rfl
-This definition is used for displaying rows of the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
-λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
 
-instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
+theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
+    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
+  classical
+  simp_rw [isCoprime_iff_add] at *
+  induction s using Finset.induction with
+  | empty =>
+      simp
+  | @insert i s _ hs =>
+      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
+      set K := ⨅ j ∈ s, J j
+      calc
+        1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
+        _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
+        _ = (1 + K) * I + K * J i  := by ring
+        _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
 
-/--
-For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
-we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
-This definition is used for displaying the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
-λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
 
-instance matrix_repr_instance :
+class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
-  has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
+  /-- Multiplication is left distributive over addition -/
+  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
+  /-- Multiplication is right distributive over addition -/
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
+{ Ring₃.toAddGroup₃ with
+  add_comm := by
+    sorry }
 
 end repr
 

tests/syntax-tests/source/Lean/LICENSE.md

@@ -0,0 +1,230 @@
+The `test.lean` file has been adpated from
+
+- multiple files of [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) under the Apache 2.0 license,
+- and https://github.com/Julian/lean-across-the-board under the MIT license.
+
+## Mathematics in Lean (Apache 2.0)
+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "{}"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright 2020 Jeremy Avigad, Patrick Massot.
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+
+## Julian/lean-across-the-board (MIT)
+
+Copyright (c) 2020 Julian Berman
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.

tests/syntax-tests/source/Lean/test.lean

@@ -1,67 +1,82 @@
-import data.matrix.notation
+import MIL.Common
-import data.vector2
+import Mathlib.Topology.Instances.Real.Defs
 
-/-!
+open Set Filter Topology
 
-Helpers that don't currently fit elsewhere...
+variable {α : Type*}
+variable (s t : Set ℕ)
+variable (ssubt : s ⊆ t)
+variable {α : Type*} (s : Set (Set α))
+-- Apostrophes are allowed in variable names
+variable (f'_x x' : ℕ)
+variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)
 
--/
+-- In the next example we could use `tauto` in each proof instead of knowing the lemmas
+example {α : Type*} (s : Set α) : Filter α :=
+  { sets := { t | s ⊆ t }
+    univ_sets := subset_univ s
+    sets_of_superset := fun hU hUV ↦ Subset.trans hU hUV
+    inter_sets := fun hU hV ↦ subset_inter hU hV }
 
-lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
-  p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
-
--- For `playfield`s, the piece type and/or piece index type.
-variables (X : Type*)
-variables [has_repr X]
 
 namespace chess.utils
 
 section repr
 
-/--
+@[class] structure One₂ (α : Type) where
-An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
+  /-- The element one -/
-for `option`, and rather, output just the value in the `some` and a custom provided
+  one : α
-`string` for `none`.
--/
-structure option_wrapper :=
-(val : option X)
-(none_s : string)
 
-instance wrapped_option_repr : has_repr (option_wrapper X) :=
+structure StandardTwoSimplex where
-⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
+  x : ℝ
+  y : ℝ
+  z : ℝ
+  x_nonneg : 0 ≤ x
+  y_nonneg : 0 ≤ y
+  z_nonneg : 0 ≤ z
+  sum_eq : x + y + z = 1
 
-variables {X}
+#check Pi.ringHom
-/--
+#check ker_Pi_Quotient_mk
-Construct an `option_wrapper` term from a provided `option X` and the `string`
+#eval 1 + 1
-that will override the `has_repr.repr` for `none`.
--/
-def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
 
--- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
+/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
-variables {m' n' : ℕ}
+  Remainder Theorem. -/
+def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
+  Ideal.Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Ideal.Quotient.mk (I i))
+    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])
 
-/--
+lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
-For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
+    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
-the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
+  rfl
-This definition is used for displaying rows of the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
-λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
 
-instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
+theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
+    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
+  classical
+  simp_rw [isCoprime_iff_add] at *
+  induction s using Finset.induction with
+  | empty =>
+      simp
+  | @insert i s _ hs =>
+      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
+      set K := ⨅ j ∈ s, J j
+      calc
+        1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
+        _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
+        _ = (1 + K) * I + K * J i  := by ring
+        _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
 
-/--
-For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
-we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
-This definition is used for displaying the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
-λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
 
-instance matrix_repr_instance :
+class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
-  has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
+  /-- Multiplication is left distributive over addition -/
+  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
+  /-- Multiplication is right distributive over addition -/
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
+{ Ring₃.toAddGroup₃ with
+  add_comm := by
+    sorry }
 
 end repr