Update mathlib, add a main function to Main.lean so lake build actually does something

Changes

2 changed files (+9/-8)

• Main.lean
  • @@ -1,5 +1,4 @@
    - import Mathlib.LinearAlgebra.Basis.VectorSpace - -- import data.nat.basic + import Mathlib inductive Vect (α : Type u) : Nat → Type u where | nil : Vect α 0
  • @@ -47,17 +46,17 @@ decreasing_by
    else exact Nat.bitwise_rec_lemma h - theorem lsb_le_i (i : Nat) : lsb i ≤ i := by + theorem lsb_le_i (i : ℕ) : lsb i ≤ i := by if h₁ : i = 0 then simp [h₁, lsb] else if h₂ : i % 2 == 1 then simp [h₁, h₂, lsb] - exact Nat.one_le_iff_ne_zero.mpr h₁ + omega else calc lsb i = 2 * lsb (i / 2) := by rw [lsb]; simp [h₁, h₂] _ ≤ 2 * (i / 2) := by simp [lsb_le_i (i / 2)] - _ ≤ i := by exact Nat.mul_div_le i 2; + _ ≤ i := Nat.mul_div_le i 2; #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
  • @@ -77,3 +76,5 @@ theorem dne {p : Prop} (h : ¬¬p) : p :=
    Or.elim (Classical.em p) (fun hp : p => hp) (fun hnp : ¬p => absurd hnp h) + + def main := IO.println "Hello, world!"
• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a655f149bb9e8ded96d946d3247b034b1ade7a25", + "rev": "c2c4e1f99f2f708b1fa11c63241024f5c2b9a70c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -55,7 +55,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "523c8ee53f7057447fc62ec14e506fda4cf63dfa", + "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,7 +75,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d", + "rev": "76408f09466811154e0e42329962de19f95d178b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",