IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger

Apache License 2.0

38 stars 13 forks source link

Add a way to pull in functions from the Haskell implementation #601

Closed Soupstraw closed 2 weeks ago

Soupstraw commented 3 weeks ago

Description

This PR makes it possible to pass the isSigned function from Haskell to Agda via the ExternalFunctions record.

closes https://github.com/IntersectMBO/formal-ledger-specifications/issues/593

Checklist

[ ] Commit sequence broadly makes sense and commits have useful messages
[ ] Any semantic changes to the specifications are documented in CHANGELOG.md
[ ] Code is formatted according to CONTRIBUTING.md
[ ] Self-reviewed the diff