## Stream: general

### Topic: Definition without body

#### Formally Verified Waffle Maker (Dec 03 2020 at 03:58):

Is it possible to get Lean to accept definitions without bodies as normal functions? So far, I have

import analysis.special_functions.trigonometric
import data.real.basic
import tactic

def lim.as_x_to_a (f : ℝ → ℝ) (a : ℝ) : ℝ

axiom lim.const_law (c : ℝ) (a : ℝ) : lim.as_x_to_a (λ (x : ℝ), c) a = c


but Lean is complaining that the axiom is an invalid definition. My goal is to define properties about lim.as_x_to_a to program its behavior, without giving the lim.as_x_to_a definition an actual body.

#### Alex J. Best (Dec 03 2020 at 04:00):

You could define the body as := sorry

#### Kenny Lau (Dec 03 2020 at 04:01):

or you can use constant

#### Kenny Lau (Dec 03 2020 at 04:01):

(which behaves exactly like axiom)

#### Formally Verified Waffle Maker (Dec 03 2020 at 04:04):

@Alex J. Best @Kenny Lau Thank you both so much!

Last updated: May 14 2021 at 03:27 UTC