[Elab.command] [14.000639s] theorem InstCombineShift279 : [...]
  [Elab.step] [0.054249s] expected type: Sort ?u.1334, term
      ∀ w : Width, [...]
    [Elab.step] [0.054242s] expected type: Sort ?u.1334, term
        forall (w : Width), [...]
      [Elab.step] [0.054184s] expected type: Sort ?u.1337, term
          ∀ C : BitVector w, [...]
        [Elab.step] [0.054180s] expected type: Sort ?u.1337, term
            forall (C : BitVector w), [...]
          [Elab.step] [0.054114s] expected type: Prop, term
              let minus_one : BitVector w := (-1).toBitVector [...]
            [Elab.step] [0.053791s] expected type: Prop, term
                let Γ : Context UserType := List.toAList [⟨42, .unit⟩] [...]
              [Elab.step] [0.012701s] expected type: Type, term
                  Context UserType
                [Elab.step] [0.012673s] expected type: Type, term
                    UserType
                  [Elab.coe] [0.012614s] adding coercion for SSA.UserType : Type → Type =?= Type
                    [Meta.synthInstance] [0.012583s] ❌ CoeT (Type → Type) SSA.UserType Type
              [Elab.step] [0.040032s] expected type: Sort ?u.1340, term
                  ∀ (e : EnvC Γ), [...]
                [Elab.step] [0.039794s] expected type: Sort ?u.2816, term
                    SSA.teval e.toEnvU [...]
                  [Elab.step] [0.039788s] expected type: Sort ?u.2816, term
                      binrel% Eq✝ [...]
                    [Elab.step] [0.018915s] expected type: <not-available>, term
                        SSA.teval e.toEnvU [...]
                      [Elab.step] [0.017885s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.REGION, term
                          [dsl_region|dsl_rgn%v0=>%v42 := [...]
                        [Elab.step] [0.017306s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.REGION, term
                            SSA.rgn✝ ([dsl_var|%v0]) [...]
                          [Elab.step] [0.016743s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                              ([dsl_bb|%v42 := [...]
                            [Elab.step] [0.016738s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                [dsl_bb|%v42 := [...]
                              [Elab.step] [0.016198s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                  ([dsl_terminator|dsl_ret %v5] <| [...]
                                [Elab.step] [0.016195s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                    [dsl_terminator|dsl_ret %v5] <| [...]
                                  [Elab.step] [0.016191s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                      ([dsl_terminator|dsl_ret %v5]) [...]
                                    [Elab.step] [0.015084s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                        (([dsl_stmt|%v42 := [...]
                                      [Elab.step] [0.015078s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                          ([dsl_stmt|%v42 := [...]
                                        [Elab.step] [0.014988s] expected type: <not-available>, term
                                            [dsl_stmt|%v42 := [...]
                                          [Elab.step] [0.014534s] expected type: <not-available>, term
                                              (((((id✝ ∘ [dsl_assign| %v42 := unit:]) ∘ [dsl_assign| %v1 := op:const C%v42]) ∘ [dsl_assign| %v2 := pair:%v0%v1]) ∘ [...]
                                            [Elab.step] [0.014529s] expected type: <not-available>, term
                                                Function.comp✝ [...]
                                              [Elab.step] [0.011884s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                  ((((id✝ ∘ [dsl_assign| %v42 := unit:]) ∘ [dsl_assign| %v1 := op:const C%v42]) ∘ [dsl_assign| %v2 := pair:%v0%v1]) ∘ [...]
                                                [Elab.step] [0.011878s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                    Function.comp✝ [...]
                    [Elab.step] [0.020476s] expected type: <not-available>, term
                        SSA.teval e.toEnvU [...]
                      [Elab.step] [0.019894s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.REGION, term
                          [dsl_region|dsl_rgn%v0=>%v42 := [...]
                        [Elab.step] [0.019371s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.REGION, term
                            SSA.rgn✝ ([dsl_var|%v0]) [...]
                          [Elab.step] [0.018878s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                              ([dsl_bb|%v42 := [...]
                            [Elab.step] [0.018873s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                [dsl_bb|%v42 := [...]
                              [Elab.step] [0.018331s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                  ([dsl_terminator|dsl_ret %v6] <| [...]
                                [Elab.step] [0.018326s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                    [dsl_terminator|dsl_ret %v6] <| [...]
                                  [Elab.step] [0.018322s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.TERMINATOR, term
                                      ([dsl_terminator|dsl_ret %v6]) [...]
                                    [Elab.step] [0.017259s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                        (([dsl_stmt|%v42 := [...]
                                      [Elab.step] [0.017254s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                          ([dsl_stmt|%v42 := [...]
                                        [Elab.step] [0.017167s] expected type: <not-available>, term
                                            [dsl_stmt|%v42 := [...]
                                          [Elab.step] [0.016729s] expected type: <not-available>, term
                                              ((((((id✝ ∘ [dsl_assign| %v42 := unit:]) ∘ [dsl_assign| %v1 := op:const minus_one%v42]) ∘ [...]
                                            [Elab.step] [0.016725s] expected type: <not-available>, term
                                                Function.comp✝ [...]
                                              [Elab.step] [0.014128s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                  (((((id✝ ∘ [dsl_assign| %v42 := unit:]) ∘ [dsl_assign| %v1 := op:const minus_one%v42]) ∘ [...]
                                                [Elab.step] [0.014124s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                    Function.comp✝ [...]
                                                  [Elab.step] [0.011778s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                      ((((id✝ ∘ [dsl_assign| %v42 := unit:]) ∘ [dsl_assign| %v1 := op:const minus_one%v42]) ∘ [...]
                                                    [Elab.step] [0.011774s] expected type: SSA.SSA InstCombine.Op SSA.SSAIndex.STMT → SSA.SSA InstCombine.Op SSA.SSAIndex.STMT, term
                                                        Function.comp✝ [...]
  [Elab.step] [2.513224s] intros w C minus_one Γ e [...]
    [Elab.step] [2.512992s] intros w C minus_one Γ e [...]
      [Elab.step] [2.510823s] simp [SSA.teval, EnvU.set, TypedUserSemantics.argUserType, TypedUserSemantics.outUserType, TypedUserSemantics.eval, [...]
[Elab.lint] [0.011076s] running linters