Skip to content

Unstructured interpretation - #163

Merged
Vtec234 merged 9 commits into
masterfrom
unstr-interp
Nov 10, 2025
Merged

Unstructured interpretation#163
Vtec234 merged 9 commits into
masterfrom
unstr-interp

Conversation

@Vtec234

@Vtec234 Vtec234 commented Oct 30, 2025

Copy link
Copy Markdown
Collaborator

Adapt soundness of interpretation to unstructured models. Closes #151.

Comment thread HoTTLean/Groupoids/Sigma.lean Outdated
@Vtec234
Vtec234 marked this pull request as ready for review November 10, 2025 06:08
@Vtec234
Vtec234 requested a review from Jlh18 November 10, 2025 06:08
@Vtec234 Vtec234 changed the title Unstructured interpretation [WIP] Unstructured interpretation Nov 10, 2025

@Jlh18 Jlh18 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Looks good to me!

@Vtec234
Vtec234 merged commit b65cda5 into master Nov 10, 2025
1 check passed
@Vtec234
Vtec234 deleted the unstr-interp branch November 10, 2025 18:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Two small breakages in Model.Unstructured.Interpretation

2 participants