Update to Lean v4.31.0-rc1

Changes

2 changed files (+4/-4)

• Dependent.lean
  • @@ -71,9 +71,9 @@ | vlam (s : String) (b : Term)
    /-- Dependent function with named first type -/ | vfn (s : String) (α β : Term) -- `Inhabited` is for panicking - -- The `BEq` things let us compare terms + -- `BEq` let us compare terms -- We need `ToExpr` for metaprogamming - deriving Inhabited, BEq, ReflBEq, LawfulBEq, Lean.ToExpr + deriving Inhabited, BEq, Lean.ToExpr open Term
  • @@ -141,7 +141,7 @@ /-- Generate a name not free in `t` or `t'` -/
    def gensym (s : String) (t t' : Term) : Id String := do let mut i := 0 -- This heuristic seems pretty fast in practice - while let s' := s ++ toString i; free s' t || free s' t' do + while (let s' := s ++ toString i; free s' t || free s' t') do i := i + 1 return s ++ toString i
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.30.0-rc2 + leanprover/lean4:v4.31.0-rc1