Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: port ModelTheory.Substructures #3913

Closed
wants to merge 47 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
a6e1e9d
feat: port ModelTheory.LanguageMap
ChrisHughes24 Mar 30, 2023
4841b4d
Initial file copy from mathport
ChrisHughes24 Mar 30, 2023
d93a4c4
automated fixes
ChrisHughes24 Mar 30, 2023
a3b2ed9
fix red
ChrisHughes24 Mar 30, 2023
e088b3b
fix yellow
ChrisHughes24 Mar 30, 2023
81a2cf1
line length
ChrisHughes24 Mar 30, 2023
27d42ff
feat: port ModelTheory.Syntax
ChrisHughes24 Mar 30, 2023
5ef5f0f
Initial file copy from mathport
ChrisHughes24 Mar 30, 2023
dc91b5f
automated fixes
ChrisHughes24 Mar 30, 2023
2a0b1fb
fix red
ChrisHughes24 Mar 30, 2023
49add2c
fix yellow
ChrisHughes24 Mar 30, 2023
b0a3a69
remove warnings
ChrisHughes24 Mar 30, 2023
3bf908a
auto: naming
ChrisHughes24 Mar 30, 2023
e3a1ebb
more comment fixing
ChrisHughes24 Mar 30, 2023
c16b8c2
line length
ChrisHughes24 Mar 30, 2023
151960b
naming and fix aligns
ChrisHughes24 Mar 30, 2023
472f2eb
Merge branch 'port/ModelTheory.LanguageMap' into port/ModelTheory.Syntax
ChrisHughes24 Mar 30, 2023
06e1f3b
fix build
ChrisHughes24 Mar 30, 2023
37b352a
feat: port ModelTheory.Semantics
ChrisHughes24 Mar 30, 2023
8a68092
Initial file copy from mathport
ChrisHughes24 Mar 30, 2023
1acb8f1
automated fixes
ChrisHughes24 Mar 30, 2023
b90ee30
start fixing
ChrisHughes24 Mar 30, 2023
644b138
more progress
ChrisHughes24 Mar 30, 2023
b48db48
fixes
ChrisHughes24 Mar 30, 2023
b7d03aa
fix yellow
ChrisHughes24 Mar 30, 2023
744ca07
fix comments
ChrisHughes24 Mar 30, 2023
2d7a0f5
revert changes to LanguageMap
ChrisHughes24 Mar 31, 2023
d371728
add simp lemma
ChrisHughes24 Apr 3, 2023
d7d4317
Merge remote-tracking branch 'origin/master' into port/ModelTheory.Se…
ChrisHughes24 Apr 17, 2023
8de6dc3
fix a little
ChrisHughes24 Apr 17, 2023
7a55451
Merge branch 'master' into port/ModelTheory.Semantics
Komyyy May 10, 2023
9c5a8c8
fix
Komyyy May 10, 2023
1488c89
fix
Komyyy May 11, 2023
83f0ec2
fix
Komyyy May 11, 2023
6b1da97
Merge branch 'FirstOrder.Language.Structure.RelMap' into port/ModelTh…
Komyyy May 11, 2023
63137e0
fix
Komyyy May 11, 2023
114192a
feat: port ModelTheory.Substructures
Komyyy May 11, 2023
4c17502
Initial file copy from mathport
Komyyy May 11, 2023
5f56f01
automated fixes
Komyyy May 11, 2023
e4fde9a
Merge branch 'port/ModelTheory.Semantics' into port/ModelTheory.Subst…
Komyyy May 11, 2023
b594922
fix
Komyyy May 11, 2023
bcabcd0
fix
Komyyy May 11, 2023
92c6221
isolated by
Komyyy May 11, 2023
26aed0a
Merge branch 'master' into port/ModelTheory.Semantics
Komyyy May 12, 2023
f627828
LHom.onTheory_model
Komyyy May 12, 2023
45879f1
Merge branch 'port/ModelTheory.Semantics' into port/ModelTheory.Subst…
Komyyy May 12, 2023
7fab5f4
Merge remote-tracking branch 'origin/master' into port/ModelTheory.Su…
ChrisHughes24 May 12, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1592,6 +1592,7 @@ import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Encoding
import Mathlib.ModelTheory.LanguageMap
import Mathlib.ModelTheory.Semantics
import Mathlib.ModelTheory.Substructures
import Mathlib.ModelTheory.Syntax
import Mathlib.NumberTheory.ADEInequality
import Mathlib.NumberTheory.Basic
Expand Down
Loading