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.ElementaryMaps #3931

Closed
wants to merge 54 commits into from
Closed

[Merged by Bors] - feat: port ModelTheory.ElementaryMaps #3931

wants to merge 54 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented May 12, 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 Komyyy added blocked-by-other-PR This PR depends on another PR which is still in the queue. 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 12, 2023
@Komyyy Komyyy mentioned this pull request May 12, 2023
Closed
2 tasks
@Komyyy Komyyy changed the title Port/ModelTheory.ElementaryMaps feat: port ModelTheory.ElementaryMaps May 12, 2023
@semorrison semorrison added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels May 12, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@Komyyy Komyyy added awaiting-CI and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels May 12, 2023
@Komyyy Komyyy mentioned this pull request May 13, 2023
Closed
1 task
@ChrisHughes24
Copy link
Member

bors merge

@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
@Komyyy @ChrisHughes24
feat: port ModelTheory.ElementaryMaps (#3931)
26d5728 
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@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.ElementaryMaps [Merged by Bors] - feat: port ModelTheory.ElementaryMaps May 13, 2023
@bors bors bot closed this May 13, 2023
@bors bors bot deleted the port/ModelTheory.ElementaryMaps branch May 13, 2023 14:18
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