Skip to content

refactor CERTS rule #922

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

Merged
williamdemeo merged 8 commits into from
Oct 1, 2025
Merged

refactor CERTS rule #922

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
3ef532e
revert CERTS rule to do CERTBASE last
williamdemeo Sep 19, 2025
d2851d8
prepare to migrate Certs.lagda{,.md}
williamdemeo Sep 26, 2025
54e15cb
migrate Certs.lagda{,.md}
williamdemeo Sep 26, 2025
92137ef
Computational-RunTraceAfterAndThen proof done!
williamdemeo Sep 27, 2025
9694bb7
prepare to migrate STS and ComputationalRelation
williamdemeo Sep 28, 2025
9ef7d76
migrate STS and ComputationalRelation
williamdemeo Sep 28, 2025
2ecec7b
incorporate Carlos's change requests
williamdemeo Sep 30, 2025
1ae6334
fix docs to reflect changes to certs rule
williamdemeo Oct 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions build-tools/static/md/mkdocs/includes/links.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,9 @@
[Auxiliary POOL transition system]: Ledger.Conway.Specification.Certs.md#auxiliary-pool-transition-system
[Calculation of Fees for Reference Scripts]: Ledger.Conway.Specification.Fees.md#sec:calculation-of-fees
[Cardano Staking: How To Stake ADA]: https://www.ledger.com/academy/cardano-staking-how-to-stake-ada
[CERT]: Ledger.Conway.Specification.Certs.md#certs-rules
[CERTS]: Ledger.Conway.Specification.Certs.md#certs-rules
[CERTS rules]: Ledger.Conway.Specification.Certs.md#certs-rules
[CERT]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
[CERTS]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
[CERTS rules]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
[CHAIN]: Ledger.Conway.Specification.Chain.md#chain-transition-system
[DELEG]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system
[ENACT]: Ledger.Conway.Specification.Enact.md#enact-transition-system
Expand Down
260 changes: 0 additions & 260 deletions src/Interface/ComputationalRelation.agda
View file
Open in desktop

This file was deleted.

Loading