tests/elab/convcalc.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            example (P : Nat → Prop) (h : P 4) : P ((1 + 1) + 2) := by

            
              conv => arg 1; calc

            
                (1 + 1) + 2

            
                _ = 2 + 2 := by simp

            
                _ = 4 := by simp

            
              exact h
	example (P : Nat → Prop) (h : P 4) : P ((1 + 1) + 2) := by
	conv => arg 1; calc
	(1 + 1) + 2
	_ = 2 + 2 := by simp
	_ = 4 := by simp
	exact h