IntersectMBO / IntersectMBO/formal-ledger-specifications
Implement FFI for ValueVector
Open
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
I think it would be good to also implement the FFI for this type in this PR, since that seems to be the main point of this particular algebra. I'd say it should map to a `Coin × List (PolicyId × String × ℕ)`, and the conversion to the Agda type should error if any of the `String`s are nonempty or there are any duplicate `PolicyId`s.
_Originally posted by @WhatisRT in https://github.com/IntersectMBO/formal-ledger-specifications/pull/757#discussion_r2054041049_
Contributor guide
Assessment
This issue has not been assessed yet.