From 885e09471db8be31499915c63951637f261f1f62 Mon Sep 17 00:00:00 2001 From: Daniel Britten Date: Tue, 29 Oct 2024 14:14:18 +1300 Subject: [PATCH] Fix default value for `hash_collision` in EVMState `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. --- Clear/EVMState.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 62a403f..6d24a3e 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -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