Remove `do` blocks from generated Lean code when possible

[JuanCoRo]

The Lean generated code currently uses more do blocks for function definitions than strictly necessary, as an example

def _742a262 : SortScheduleConst → SortSchedule → Option SortInt
  | SortScheduleConst.Rb_SCHEDULE_ScheduleConst, SortSchedule.CONSTANTINOPLE_EVM => do
    let _Val0 <- «_*Int_» 2 1000000000000000000
    return _Val0
  | _, _ => none

could be defined as

def _742a262 : SortScheduleConst → SortSchedule → Option SortInt
  | SortScheduleConst.Rb_SCHEDULE_ScheduleConst, SortSchedule.CONSTANTINOPLE_EVM => «_*Int_» 2 1000000000000000000
  | _, _ => none

In particular, unless the do block is used to chain functions that return an Option type, it can be removed.

Additionally, functions which depend on total functions could be redefined without the do block once their dependencies are stripped of the Option return type. For example

def _432555e : SortWordStack → SortInt → Option SortInt
    | SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Gen0 WS, SIZE => do
      let _Val0 <- «_+Int_» SIZE 1
      let _Val1 <- sizeWordStackAux WS _Val0
      return _Val1
    | _, _ => none

Once «_+Int_» and sizeWordStackAux return a SortInt type instead of Option SortInt, it could be redefined as the following or similar

def _432555e : SortWordStack → SortInt → SortInt
    | SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Gen0 WS, SIZE =>
      let _Val0 := «_+Int_» SIZE 1
      sizeWordStackAux WS _Val0
    | _, _ => 0