Skip to content

Notebook elaboration for equality types#1061

Merged
epatters merged 8 commits intomainfrom
notebook_elaborator
Mar 21, 2026
Merged

Notebook elaboration for equality types#1061
epatters merged 8 commits intomainfrom
notebook_elaborator

Conversation

@KevinDCarlson
Copy link
Copy Markdown
Collaborator

@KevinDCarlson KevinDCarlson commented Feb 19, 2026 •
edited
Loading

Depends on #1047 and #1060. Elaboration of notebooks containing equations to the type theory. Note that the diffs to modules in tt other than notebook_eval itself are spurious, due to the double parentage.

KevinDCarlson
KevinDCarlson commented Feb 19, 2026
View reviewed changes
Comment thread packages/catlog/src/dbl/discrete/model.rs Outdated
@KevinDCarlson KevinDCarlson changed the base branch from main to equations_in_notebook_types February 19, 2026 23:31
@epatters epatters changed the title Notebook elaborator Notebook elaboration for equality types Feb 20, 2026
@epatters epatters added enhancement New feature or request core Rust core for categorical logic and general computation labels Feb 20, 2026
@KevinDCarlson KevinDCarlson force-pushed the equations_in_notebook_types branch 2 times, most recently from 0f76c07 to 342933e Compare February 27, 2026 19:06
@KevinDCarlson KevinDCarlson force-pushed the equations_in_notebook_types branch from cffcd0d to 20606f3 Compare March 10, 2026 19:30
Base automatically changed from equations_in_notebook_types to main March 16, 2026 22:08
@epatters
Copy link
Copy Markdown
Member

epatters commented Mar 16, 2026

Now that #1047 and #1060 have been merged, you'll need to rebase this one and fix the merge conflicts.

@epatters epatters marked this pull request as draft March 16, 2026 22:14
@epatters epatters marked this pull request as ready for review March 19, 2026 23:13
@KevinDCarlson
Copy link
Copy Markdown
Collaborator Author

KevinDCarlson commented Mar 19, 2026

Now that #1047 and #1060 have been merged, you'll need to rebase this one and fix the merge conflicts.

Done.

epatters
epatters requested changes Mar 20, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@epatters epatters left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Thanks Kevin, this looks good modulo the preexisting design problem that you're having to work around. See my comments below for more context.

Comment thread packages/catlog/examples/tt/notebook/commutative_square.json Outdated
Comment thread packages/catlog/src/tt/notebook_elab.rs Outdated
Comment thread packages/catlog/src/tt/notebook_elab.rs Outdated
Comment thread packages/catlog/src/one/path.rs Outdated
Comment thread packages/catlog/src/dbl/model.rs Outdated

/// Equation between morphisms has one or more errors.
Eq(usize, NonEmpty<InvalidPathEq>),
Eqn(Option<usize>, NonEmpty<InvalidPathEq>),
Copy link
Copy Markdown
Member

@epatters epatters Mar 20, 2026

Choose a reason for hiding this comment

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

Why is this an Option now?

Edit: Ok, from the comment below, I now remember what's going. Can you please put a FIXME in the comment above as a reminder to undo this once we've fixed #1017.

@epatters epatters merged commit 13fa7ed into main Mar 21, 2026
15 checks passed
@epatters epatters deleted the notebook_elaborator branch March 21, 2026 18:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@epatters epatters epatters approved these changes

Assignees

No one assigned

Labels

core Rust core for categorical logic and general computation enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@KevinDCarlson @epatters