Update to Lean 4.32.0 with the new do elaborator

Changes

4 changed files (+10/-10)

• Main.lean
  • @@ -3,9 +3,6 @@ import Raylean
    -- See https://github.com/funexists/raylean/ PRs #61, #62, #63 for the stuff that I upstreamed to Raylean - -- This fixes the "unexpected error when elaborating 'let'" bug - set_option backward.do.legacy false - open Raylean Types -- Random stuff that should be in the Lean standard library but isn't?
  • @@ -1170,6 +1167,9 @@ | "prod" :: _ =>
    for b in (← get).buildings do if b.production > 0 then IO.println s!"Building {b.variant} at {b.pos}: {b.production}" + -- | "cheat" :: _ => + -- let b := (← get).buildings + -- modifyf peeps (·.map fun p ↦ { p with pos := b[p.dest]!.entrance }) | "tl" :: A => if h : A.length ≥ 6 then let A := A.map String.toNat!
• flake.lock
  • @@ -41,16 +41,16 @@ }
    }, "nixpkgs": { "locked": { - "lastModified": 1782856423, - "narHash": "sha256-ehxnpv3BZodGJeFPIXnDs4GpHdkqU3+MtW6OCwRzwnM=", + "lastModified": 1783977245, + "narHash": "sha256-jQMgFO5+iG8B2Vo6y++O66xeoPIz49CMPfed3r571Xs=", "owner": "i-love-lean", "repo": "nixpkgs", - "rev": "ac5524f9353a9a596e0dbef34438af5f528fcd2b", + "rev": "5b17b7764b07f83e91869e3cfab4507d6d7accab", "type": "github" }, "original": { "owner": "i-love-lean", - "ref": "lean4-bump", + "ref": "lean4-bump2", "repo": "nixpkgs", "type": "github" }
• flake.nix
  • @@ -2,8 +2,8 @@ {
    description = "An OpenTTD-like game written in Lean"; inputs = { - # TODO: Change this back to nixos-unstable once it gets lean4 v4.31.0 - nixpkgs.url = "github:i-love-lean/nixpkgs/lean4-bump"; + # TODO: Change this back to nixos-unstable once it gets lean4 v4.32.0 + nixpkgs.url = "github:i-love-lean/nixpkgs/lean4-bump2"; nixgl = { url = "github:nix-community/nixGL"; inputs.nixpkgs.follows = "nixpkgs";
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.31.0 + leanprover/lean4:v4.32.0