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