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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: port ModelTheory.Skolem #3951

Closed
wants to merge 61 commits into from
Closed

[Merged by Bors] - feat: port ModelTheory.Skolem #3951

wants to merge 61 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented May 13, 2023 •
edited by github-actions bot

@ChrisHughes24
feat: port ModelTheory.LanguageMap
a6e1e9d
@ChrisHughes24
Initial file copy from mathport
4841b4d
@ChrisHughes24
automated fixes
d93a4c4 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@ChrisHughes24
fix red
a3b2ed9
@ChrisHughes24
fix yellow
e088b3b
@ChrisHughes24
line length
81a2cf1
@ChrisHughes24
feat: port ModelTheory.Syntax
27d42ff
@ChrisHughes24
Initial file copy from mathport
5ef5f0f
@ChrisHughes24
automated fixes
dc91b5f 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@ChrisHughes24
fix red
2a0b1fb
@ChrisHughes24
fix yellow
49add2c
@ChrisHughes24
remove warnings
b0a3a69
@ChrisHughes24
auto: naming
3bf908a
@ChrisHughes24
more comment fixing
e3a1ebb
@ChrisHughes24
line length
c16b8c2
@ChrisHughes24
naming and fix aligns
151960b
@ChrisHughes24
Merge branch 'port/ModelTheory.LanguageMap' into port/ModelTheory.Syntax
472f2eb
@ChrisHughes24
fix build
06e1f3b
@ChrisHughes24
feat: port ModelTheory.Semantics
37b352a
@ChrisHughes24
Initial file copy from mathport
8a68092
@ChrisHughes24
automated fixes
1acb8f1 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@ChrisHughes24
start fixing
b90ee30
@ChrisHughes24
more progress
644b138
@ChrisHughes24
fixes
b48db48
@ChrisHughes24
fix yellow
b7d03aa
@ChrisHughes24
fix comments
744ca07
@ChrisHughes24
revert changes to LanguageMap
2d7a0f5
@ChrisHughes24
add simp lemma
d371728
@ChrisHughes24
Merge remote-tracking branch 'origin/master' into port/ModelTheory.Se…
d7d4317 
…mantics
@ChrisHughes24
fix a little
8de6dc3
Komyyy added 14 commits May 12, 2023 11:23
@Komyyy
Merge branch 'port/ModelTheory.Substructures' into port/ModelTheory.E…
ffdfd56 
…lementaryMaps
@Komyyy
fix
5f85711
@Komyyy
lint
de521ea
@Komyyy
Merge branch 'master' into port/ModelTheory.Semantics
26aed0a
@Komyyy
LHom.onTheory_model
f627828
@Komyyy
Merge branch 'port/ModelTheory.Semantics' into port/ModelTheory.Subst…
45879f1 
…ructures
@Komyyy
Merge branch 'port/ModelTheory.Substructures' into port/ModelTheory.E…
53c677a 
…lementaryMaps
@Komyyy
Merge branch 'master' into port/ModelTheory.ElementaryMaps
02c3a2e
@Komyyy
feat: port ModelTheory.Skolem
0ce4b01
@Komyyy
Initial file copy from mathport
69d3401
@Komyyy
automated fixes
edd89e0 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy
Merge branch 'port/ModelTheory.ElementaryMaps' into port/ModelTheory.…
9465182 
…Skolem
@Komyyy
fix
03756a2
@Komyyy
fix
a560349
@Komyyy Komyyy added awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. awaiting-CI labels May 13, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label May 13, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label May 13, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@ChrisHughes24
Copy link
Member

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 13, 2023
bors bot pushed a commit that referenced this pull request May 13, 2023
@ChrisHughes24 @Komyyy
feat: port ModelTheory.Skolem (#3951)
21ac3b5 
Co-authored-by: Komyyy <pol_tta@outlook.jp>
@bors
Copy link

bors bot commented May 13, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port ModelTheory.Skolem [Merged by Bors] - feat: port ModelTheory.Skolem May 13, 2023
@bors bors bot closed this May 13, 2023
@bors bors bot deleted the port/ModelTheory.Skolem branch May 13, 2023 14:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Komyyy @semorrison @ChrisHughes24