Definition without body

Stream: general

[Formally Verified Waffle Maker]

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]

You could define the body as := sorry

[Kenny Lau]

or you can use constant

[Kenny Lau]

(which behaves exactly like axiom)

[Formally Verified Waffle Maker]

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