Skip to content
Snippets Groups Projects
Commit 5e9a8aed authored by Dan Frumin's avatar Dan Frumin
Browse files

Remove unnecessary arguments from `ResolveProphS`.

parent ac6dc97b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/lang.v
+ 1
− 3
View file @ 5e9a8aed
...@@ -557,9 +557,7 @@ Inductive head_step : expr → state → list observation → expr → state → ...@@ -557,9 +557,7 @@ Inductive head_step : expr → state → list observation → expr → state →
[] []
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ) (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
[] []
| ResolveProphS e1 p e2 v σ : | ResolveProphS p v σ :
to_val e1 = Some (LitV $ LitProphecy p) →
to_val e2 = Some v →
head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
[(p, v)] [(p, v)]
(Val $ LitV LitUnit) σ []. (Val $ LitV LitUnit) σ [].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment