Skip to content

Commit

Permalink
Fix default value for hash_collision in EVMState
Browse files Browse the repository at this point in the history
`false` is a `Bool`. The intended default value.
`False` is the `Prop` representing a contradiction, not the intended default value of `hash_collision`, but since `False` is a decidable proposition, Lean automatically treats this as `decide False` which is a `Bool`.
Although we can actually prove `false = False` in Lean, using `false` directly is preferable.
  • Loading branch information
Coda-Coda committed Oct 29, 2024
1 parent 29e3c76 commit 885e094
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Clear/EVMState.lean
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ structure EVMState : Type where
deriving DecidableEq

instance : Inhabited EVMState :=
⟨ ∅ , default, default , ∅ , default, ∅ , default , False
⟨ ∅ , default, default , ∅ , default, ∅ , default , false

abbrev EVM := EVMState

Expand Down

0 comments on commit 885e094

Please sign in to comment.