Merge `improvement/iprover-for-symmetry` of pull request #61 into `master`
Switch from `blast` to `iprover` for symmetry proofs
Switch from `blast` to `iprover` for symmetry proofs
by (intro exI conjI, use in assumption) (fastforce intro: rev_bexI)
qed
qed
qed (respectful, blast)
qed (respectful, iprover)
end
using equality_in_universe
by (intro exI conjI, use in assumption) (fastforce intro: rev_bexI)
qed
qed (respectful, blast)
qed (respectful, iprover)
locale synchronous_transition_system =
transition_system \<open>transition\<close>
SCP-4880 GetTransaction Query
* Moved the JSON serialization of the types of the UtxoIndexer in `marconi-chain-index` instead of `marconi-mamba` * Updated README of `marconi-mamba` Co-authored-by: koslambrou <[email protected]>
3993: PLT-106: Add encoder and decoder for `LedgerState` r=zliu41 a=zliu41 One use case is for `foldBlocks` to checkpoint the ledger state to avoid having to start from Genisys. cc `@JaredCorduan` Co-authored-by: Ziyang Liu <[email protected]>
Co-authored-by: koslambrou <[email protected]>
This should get ahold of all the applied plutus scripts in a transaction to profile them externally. For now, this is a just a frankenstein evaluateTx.
Add links to ledger CDDL specs, and warn about lack of information about HFC.
- Renamed the module names from Marconi.JsonRpc to Network.JsonRpc - Renamed `marconi` to `marconi-chain-index` - Renamed `rewindable-index` package to `marconi-core` and changed corresponding module names accordingly - Renamed marconi-mamba module names to match those of corresponding package name Co-authored-by: koslambrou <[email protected]>
- Renamed the module names from Marconi.JsonRpc to Network.JsonRpc - Renamed `marconi` to `marconi-chain-index` - Renamed `rewindable-index` package to `marconi-core` and changed corresponding module names accordingly - Renamed marconi-mamba module names to match those of corresponding package name Co-authored-by: koslambrou <[email protected]>
Co-authored-by: Jamie Bertram <[email protected]>