Skip to content

[ deprecate ] Relation/Binary.PropositionalEquality.inspect and README.Inspect (#1580 / #1630 / #1930 redux)#2981

Merged
JacquesCarette merged 5 commits intoagda:experimentalfrom
jamesmckinna:deprecate-Inspect+README
Apr 22, 2026
Merged

[ deprecate ] Relation/Binary.PropositionalEquality.inspect and README.Inspect (#1580 / #1630 / #1930 redux)#2981
JacquesCarette merged 5 commits intoagda:experimentalfrom
jamesmckinna:deprecate-Inspect+README

Conversation

@jamesmckinna
Copy link
Copy Markdown
Collaborator

Clean do-over of many previous versions of this, most recently #2934 / #2928

@jamesmckinna
Copy link
Copy Markdown
Collaborator Author

jamesmckinna commented Apr 16, 2026

oops, README.Data.Wrap... who would have thought? (I guess this failure wasn't caught before in #2934 because of the failure wrt README.Inspect... further justification for amalgamating under one roof!?)

@JacquesCarette
Copy link
Copy Markdown
Collaborator

So I was able to use the menus to restart just the versions that had failed - and they pass now.

Comment thread doc/README/Inspect.agda
@gallais gallais changed the base branch from master to experimental April 22, 2026 14:01
@JacquesCarette JacquesCarette merged commit 2f84dcc into agda:experimental Apr 22, 2026
45 of 58 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants