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
Bryan Gin-ge Chen (Jun 30 2020 at 15:49):
import analysis.special_functions.pow to the top of your file.
Bryan Gin-ge Chen (Jun 30 2020 at 15:50):
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