Revision #2952 → #3445 · back to history
modifiedProof by contradiction (non-constructive)09a1ae547671
| Field | From #2952 | To #3445 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Mathlib uses classical proof by contradiction via Lean core's `Classical.byContradiction` (referenced from `Mathlib.Logic.Basic`) but does not classify it as non-constructive. | Mathlib uses classical proof by contradiction via Lean core's `Classical.byContradiction` (in `Init.Classical`) but does not classify it as non-constructive. |
modifiedCartesian closed categories correspond to typed λ-calculus0bd29c97f2f7
| Field | From #2952 | To #3445 |
|---|
| mathlib.decl | CategoryTheory.CartesianClosed | CategoryTheory.MonoidalClosed |
| mathlib.module | Mathlib.CategoryTheory.Closed.Cartesian | Mathlib.CategoryTheory.Monoidal.Closed.Basic |
| note | Mathlib defines Cartesian closed categories but does not formalize the equivalence with simply typed λ-calculus. | Mathlib defines cartesian closed categories through `MonoidalClosed` on a `CartesianMonoidalCategory` (the former `CartesianClosed` class was deprecated), but does not formalize the correspondence with the simply typed λ-calculus. |
modifiedVector-length dependent type (dot product)698387ab64f4
| Field | From #2952 | To #3445 |
|---|
| mathlib.module | Mathlib.Data.Vector.Basic | Mathlib.Data.Vector.Defs |
addedKleene–Rosser paradoxb924fadd28db
addedHigher-order logic9e3b0cd2d7c1
addedJudgmental (definitional) equality386de992ea5c
addedContext weakening243d73c69265
addedType universe hierarchy2013eb0c0383
addedCategorical logic (interplay of categories and type theory)9ed3acca717e
addedAnonymous function12fedcae960d
addedSuccessor function on ℕ1119a388631e
addedLength-indexed list (dependent list type)e9669bbbafaf
addedScott encoding of inductive typesfe547180fecb
addedChurch encoding of numbers8fad21792912
addedSubtyping3b268712ab0a
addedCategorial grammar2f955c18a02a