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


            
            opaque f : Nat → Nat

            
            @[simp] axiom f_ax : f (no_index 0) = 1

            
            example : f ((fun x => x) 0) = 1 := by

            
              fail_if_success simp -beta -- should fail

            
              simp
	opaque f : Nat → Nat
	@[simp] axiom f_ax : f (no_index 0) = 1
	example : f ((fun x => x) 0) = 1 := by
	fail_if_success simp -beta -- should fail
	simp