Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
concordium
smart-contract-interactions
Commits
5a4057c6
Commit
5a4057c6
authored
Oct 25, 2019
by
Jakob Botsch Nielsen
Browse files
Unfold set_chain_contract_state more aggressively
parent
86df9fd4
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/Blockchain.v
View file @
5a4057c6
...
...
@@ -1056,6 +1056,11 @@ Arguments build_contract {_ _ _ _ _ _ _}.
Arguments
ContractInterface
{
_
}
_.
Arguments
build_contract_interface
{
_
_
_
_
}
.
(
*
set_chain_contract_state
updates
a
map
(
function
)
by
returning
a
new
map
(
function
).
If
this
function
is
immediately
applied
to
a
key
,
then
unfold
it
.
*
)
Arguments
set_chain_contract_state
{
_
}
_
_
_
/
.
Ltac
destruct_chain_step
:=
match
goal
with
|
[
step
:
ChainStep
_
_
|-
_
]
=>
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment