Andre Knispel
Andre Knispel
We have `POOLREAP` in Shelley, and a lot of the logic for refunding GA deposits is shared with that. So it makes sense to implement that STS, but rename it...
# Description This introduces a dependency of the new [agda-sets](https://github.com/input-output-hk/agda-sets). I also did some refactoring as part of this, which is where most changes come from. I've requested reviews from...
This ticket is for keeping track of issues discovered or fixed recently. - #490 (Done, waiting on conformance) - #491 (WIP, estimate: 2 days) - #508 - #510 - #511...
We have two models right now, one under `Ledger` and one under `Ledger.Conway.Conformance`. They differ by some logic being moved from `CERTS` into `UTXO` but are otherwise identical. This means...
- [ ] None of the `Ledger.Conway.Conformance` modules need to be literate Agda files, we probably won't compile those into a pdf. Removing all that stuff also should help restore...
This issue is for discussing the high-level roadmap for this project. Note that we may drop things off of here if we decide against them in the future. # Features...
Once Agda 2.7 makes it into [nixpkgs master](https://raw.githubusercontent.com/NixOS/nixpkgs/master/pkgs/development/haskell-modules/hackage-packages.nix) we should update (see the bottom of `CONTRIBUTING.md` on how to update `agda-nixpkgs`). This will unblock merging #488.
When a variable is in scope whose type contains a hole, it seems that at least some instances aren't available for instance resolution. Here are two examples: ```agda module Test...
Here's a minimal reproducer: ```agda module Test where open import Agda.Builtin.Nat record R : Set where record S : Set where field s : Nat module X (r : R)...
We should think about how we want to model the types of transactions in the presence of subtransactions. Some nice to haves are: - will not require "global" code changes...