input-output-hk / input-output-hk/Lean-blaster
Fix issue when only sorry tactic is used with blaster executed with only-optimize option
Open
area: optimizer
area:tactic
bug
- Dominant language
- Lean
- Stars
- 57
- Forks
- 11
- Avg merge
- 1d 5h
- Merged PRs (30d)
- 10
Description
```lean
theorem sto8 :
∀ (x : ProcessSCInput) (s : ComputeReserve),
isSellSCOrder x →
validOrderInput x →
resultToComputeReserve (fromHaltState $ compiledProcessSCOrder x) = some s →
validSellSC x s := by
intro x s;
blaster (only-optimize: 1)
by_cases x.state.crN_SC = 0 <;>
by_cases x.state.crN_RC = 0
. sorry
. sorry
. sorry
. sorry
```
---
**Transferred from:** input-output-hk/sc-fvt#506
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.