Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(model_theory/types): Complete types over a theory #16548

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat(model_theory/types): Complete types over a theory #16548

wants to merge 14 commits into from

Conversation

awainverse
Copy link
Collaborator

@awainverse awainverse commented Sep 18, 2022 •
edited
Loading

Defines the space of complete types over a particular theory in a particular type of variables

Open in Gitpod

@awainverse awainverse added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Sep 18, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 19, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@awainverse awainverse changed the title feat(model_theory/types): The space of complete types feat(model_theory/types): Complete types over a theory Sep 19, 2022
@awainverse awainverse mentioned this pull request Sep 20, 2022
Closed
1 task
jcommelin
jcommelin approved these changes Sep 20, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 20, 2022
bors bot pushed a commit that referenced this pull request Sep 20, 2022
@awainverse
feat(model_theory/types): Complete types over a theory (#16548)
95d6715 
Defines the space of complete types over a particular theory in a particular type of variables
@bors
Copy link

bors bot commented Sep 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(model_theory/types): Complete types over a theory [Merged by Bors] - feat(model_theory/types): Complete types over a theory Sep 20, 2022
@bors bors bot closed this Sep 20, 2022
@bors bors bot deleted the complete_type branch September 20, 2022 08:56
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
@awainverse @b-mehta
feat(model_theory/types): Complete types over a theory (#16548)
65521b0 
Defines the space of complete types over a particular theory in a particular type of variables
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@fpvandoorn fpvandoorn Awaiting requested review from fpvandoorn

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@awainverse @mathlib-dependent-issues-bot @jcommelin @leanprover-community-bot-assistant