remove `\xspace`s, upgrade `\ref`s and `\cite`s
Home /
IntersectMBO /
formal-ledger-specifications
Feb 15, 2-3 AM (0)
Feb 15, 3-4 AM (0)
Feb 15, 4-5 AM (0)
Feb 15, 5-6 AM (0)
Feb 15, 6-7 AM (0)
Feb 15, 7-8 AM (0)
Feb 15, 8-9 AM (0)
Feb 15, 9-10 AM (0)
Feb 15, 10-11 AM (0)
Feb 15, 11-12 PM (0)
Feb 15, 12-1 PM (0)
Feb 15, 1-2 PM (0)
Feb 15, 2-3 PM (0)
Feb 15, 3-4 PM (0)
Feb 15, 4-5 PM (0)
Feb 15, 5-6 PM (0)
Feb 15, 6-7 PM (0)
Feb 15, 7-8 PM (0)
Feb 15, 8-9 PM (0)
Feb 15, 9-10 PM (0)
Feb 15, 10-11 PM (0)
Feb 15, 11-12 AM (0)
Feb 16, 12-1 AM (0)
Feb 16, 1-2 AM (0)
Feb 16, 2-3 AM (0)
Feb 16, 3-4 AM (0)
Feb 16, 4-5 AM (0)
Feb 16, 5-6 AM (0)
Feb 16, 6-7 AM (0)
Feb 16, 7-8 AM (0)
Feb 16, 8-9 AM (0)
Feb 16, 9-10 AM (0)
Feb 16, 10-11 AM (0)
Feb 16, 11-12 PM (0)
Feb 16, 12-1 PM (0)
Feb 16, 1-2 PM (0)
Feb 16, 2-3 PM (0)
Feb 16, 3-4 PM (0)
Feb 16, 4-5 PM (0)
Feb 16, 5-6 PM (0)
Feb 16, 6-7 PM (0)
Feb 16, 7-8 PM (0)
Feb 16, 8-9 PM (0)
Feb 16, 9-10 PM (0)
Feb 16, 10-11 PM (0)
Feb 16, 11-12 AM (0)
Feb 17, 12-1 AM (0)
Feb 17, 1-2 AM (0)
Feb 17, 2-3 AM (0)
Feb 17, 3-4 AM (0)
Feb 17, 4-5 AM (0)
Feb 17, 5-6 AM (0)
Feb 17, 6-7 AM (0)
Feb 17, 7-8 AM (1)
Feb 17, 8-9 AM (0)
Feb 17, 9-10 AM (0)
Feb 17, 10-11 AM (2)
Feb 17, 11-12 PM (0)
Feb 17, 12-1 PM (2)
Feb 17, 1-2 PM (1)
Feb 17, 2-3 PM (3)
Feb 17, 3-4 PM (2)
Feb 17, 4-5 PM (1)
Feb 17, 5-6 PM (0)
Feb 17, 6-7 PM (0)
Feb 17, 7-8 PM (0)
Feb 17, 8-9 PM (0)
Feb 17, 9-10 PM (0)
Feb 17, 10-11 PM (0)
Feb 17, 11-12 AM (0)
Feb 18, 12-1 AM (0)
Feb 18, 1-2 AM (0)
Feb 18, 2-3 AM (0)
Feb 18, 3-4 AM (0)
Feb 18, 4-5 AM (0)
Feb 18, 5-6 AM (0)
Feb 18, 6-7 AM (0)
Feb 18, 7-8 AM (0)
Feb 18, 8-9 AM (0)
Feb 18, 9-10 AM (0)
Feb 18, 10-11 AM (0)
Feb 18, 11-12 PM (0)
Feb 18, 12-1 PM (0)
Feb 18, 1-2 PM (3)
Feb 18, 2-3 PM (2)
Feb 18, 3-4 PM (0)
Feb 18, 4-5 PM (0)
Feb 18, 5-6 PM (0)
Feb 18, 6-7 PM (0)
Feb 18, 7-8 PM (0)
Feb 18, 8-9 PM (0)
Feb 18, 9-10 PM (0)
Feb 18, 10-11 PM (1)
Feb 18, 11-12 AM (0)
Feb 19, 12-1 AM (0)
Feb 19, 1-2 AM (0)
Feb 19, 2-3 AM (0)
Feb 19, 3-4 AM (0)
Feb 19, 4-5 AM (0)
Feb 19, 5-6 AM (0)
Feb 19, 6-7 AM (0)
Feb 19, 7-8 AM (4)
Feb 19, 8-9 AM (0)
Feb 19, 9-10 AM (2)
Feb 19, 10-11 AM (3)
Feb 19, 11-12 PM (0)
Feb 19, 12-1 PM (0)
Feb 19, 1-2 PM (0)
Feb 19, 2-3 PM (0)
Feb 19, 3-4 PM (1)
Feb 19, 4-5 PM (0)
Feb 19, 5-6 PM (0)
Feb 19, 6-7 PM (0)
Feb 19, 7-8 PM (0)
Feb 19, 8-9 PM (0)
Feb 19, 9-10 PM (1)
Feb 19, 10-11 PM (0)
Feb 19, 11-12 AM (0)
Feb 20, 12-1 AM (0)
Feb 20, 1-2 AM (0)
Feb 20, 2-3 AM (0)
Feb 20, 3-4 AM (0)
Feb 20, 4-5 AM (0)
Feb 20, 5-6 AM (0)
Feb 20, 6-7 AM (0)
Feb 20, 7-8 AM (0)
Feb 20, 8-9 AM (2)
Feb 20, 9-10 AM (0)
Feb 20, 10-11 AM (2)
Feb 20, 11-12 PM (4)
Feb 20, 12-1 PM (2)
Feb 20, 1-2 PM (0)
Feb 20, 2-3 PM (0)
Feb 20, 3-4 PM (2)
Feb 20, 4-5 PM (0)
Feb 20, 5-6 PM (0)
Feb 20, 6-7 PM (0)
Feb 20, 7-8 PM (0)
Feb 20, 8-9 PM (1)
Feb 20, 9-10 PM (0)
Feb 20, 10-11 PM (0)
Feb 20, 11-12 AM (0)
Feb 21, 12-1 AM (0)
Feb 21, 1-2 AM (0)
Feb 21, 2-3 AM (0)
Feb 21, 3-4 AM (0)
Feb 21, 4-5 AM (0)
Feb 21, 5-6 AM (0)
Feb 21, 6-7 AM (0)
Feb 21, 7-8 AM (0)
Feb 21, 8-9 AM (0)
Feb 21, 9-10 AM (0)
Feb 21, 10-11 AM (3)
Feb 21, 11-12 PM (2)
Feb 21, 12-1 PM (0)
Feb 21, 1-2 PM (0)
Feb 21, 2-3 PM (0)
Feb 21, 3-4 PM (2)
Feb 21, 4-5 PM (0)
Feb 21, 5-6 PM (0)
Feb 21, 6-7 PM (0)
Feb 21, 7-8 PM (0)
Feb 21, 8-9 PM (0)
Feb 21, 9-10 PM (0)
Feb 21, 10-11 PM (0)
Feb 21, 11-12 AM (0)
Feb 22, 12-1 AM (1)
Feb 22, 1-2 AM (0)
Feb 22, 2-3 AM (0)
50 commits this week
Feb 15, 2025
-
Feb 22, 2025
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&s=80)
Updated for 15d82b0fbaffe8359669cb874c72ea558c54ce15
Generate code for GH-688
Add explanation for a refactor of the symbol ≡?
- Refactor the code to use `Connected` for ≡? from stdlib
Hide TransactionStructure
Generate code for a59c6aaba7b40d3c5f81b24831f14fd791d950ef
Merge branch 'master' into 683-review-the-conway-diff-spec
Reformat Fee Calculation
- remove visible uses of with - remove visible use of wellfounded recursion - rearrange text - remove some functions which are available from stdlib
improve .gitignore and other minor possible improvements
Updated for d7aea0277e56d682c432273d56fed8ca9297cf48
Fix duplication introduced by #659 (#692)
Fix duplication introduced by #659
Merge branch 'master' into 681-use-latex-best-practices-and-packages
Updated for 3295ab2a2aad061fcc4ee10f5cb650af29fb92aa
Generate code for GH-659
Reference previous specifications & other material (#659)
This addresses #341. * add more references * include links to the Agda module for each section * Update src/Ledger/Introduction.lagda * Update src/Ledger/Utxow.lagda * add macros for consistent reference to cips * Replace \Ledger* commands by a parameterised command \LedgerModule * detokenize macro so href won't append `pdf` to url * Fix citations and import of Notation.tex * move EssentialAgda module outside Ledger module * add new macro for referencing official Agda docs * uncomment paragraph that may have been deleted accidentally; (remove it later if it was deleted on purpose) * final edits to remove some warnings in tex output --------- Co-authored-by: Andre Knispel <[email protected]> Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
Generate code for 2acac55a9e833418a83d864b3f3e14de98cc777b
Refactor conformance to use GOV rule from Ledger
Inline Equivalence.Base
Merge branch '341-reference-previous-specifications-other-material' of github.com:IntersectMBO/formal-ledger-specifications into 341-reference-previous-specifications-other-material
Revert changes to Lib.hs
Updated for 038817e91d41110e3bdab1c7e5fcfdb0c4607c83
Generate code for GH-684