Code

fix: allow generalization in let#3060

Code

Merged

Kha merged 5 commits intoleanprover:masterleanprover/lean4:masterfrom eric-wieser:let-generalizationeric-wieser/lean4:let-generalizationCopy head branch name to clipboardJan 23, 2024

+17-5

Commits

Commits on Dec 13, 2023

• fix: allow generalization in let

  eric-wieser

  committed
  41d1af1

  Copy full SHA for 41d1af1

• missing type

  eric-wieser

  committed
  2d29fd5

  Copy full SHA for 2d29fd5

• add a test

  eric-wieser

  committed
  4d12284

  Copy full SHA for 4d12284

Commits on Dec 15, 2023

• Merge remote-tracking branch 'origin/nightly-with-mathlib' into let-generalization

  eric-wieser

  committed
  d8d54db

  Copy full SHA for d8d54db

Commits on Jan 4, 2024

• Merge remote-tracking branch 'upstream/nightly-with-mathlib' into let-generalization

  eric-wieser

  committed
  8822bfd

  Copy full SHA for 8822bfd