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


            
            def test : (λ x : Nat => id (id x)) = λ x => x := by

            
              conv in (id _) =>

            
                trace_state

            
                simp
	def test : (λ x : Nat => id (id x)) = λ x => x := by
	conv in (id _) =>
	trace_state
	simp