# Zulip Chat Archive

## Stream: general

### Topic: failed to synthesize type class instance error

#### James Arthur (Jun 30 2020 at 15:44):

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 (Jun 30 2020 at 15:49):

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 (Jun 30 2020 at 15:49):

Add `import analysis.special_functions.pow`

to the top of your file.

#### Bryan Gin-ge Chen (Jun 30 2020 at 15:50):

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

#### Bryan Gin-ge Chen (Jun 30 2020 at 15:53):

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 (Jun 30 2020 at 16:00):

Thankyou both, it works now!

Last updated: May 17 2021 at 22:15 UTC