Dependently typed blockchain experiments in Idris.
Blockchainmodule implements a blockchain (cryptographic linked list) with type guarantee that hashes are correct and the chain is not compromised.
Proof of type? :)
Work-in-progress
I am using idris 1.2 This project includes make file with configuration to build and run tests. To use interactive repl:
> cd src
> idris repl --package contrib