failed to synthesize type class instance error

Stream: general

[James Arthur]

I am defining a radius on a wonky square and it is giving me some errors. Here is the definition:

import tactic
import data.real.basic
import data.complex.exponential

noncomputable theory
open_locale classical

open real

def radius (x m : ℝ) := 1 / ( |sin x| ^ m + |cos x| ^ m ) ^ (1/m)

and the error:

failed to synthesize type class instance for
x m : ℝ
⊢ has_pow ℝ ℝ

why is it doing this and how do I remedy it?

[Simon Hudon]

I'm not sure if that instance exists. First step to debug this problem is using #print instances has_pow. It will show you all the instances that exist. It might be that you might define your own using exp.

[Bryan Gin-ge Chen]

Add import analysis.special_functions.pow to the top of your file.

[Bryan Gin-ge Chen]

See src#real.has_pow (and src#real.rpow right above it).

[Bryan Gin-ge Chen]

The error message means that Lean could not figure out how to interpret ^ as an operator on two real numbers. The instance that helps Lean figure out what ^ means on two real numbers turns out to be defined in analysis.special_functions.pow, so importing it should fix things.

[James Arthur]

Thankyou both, it works now!