Zulip Chat Archive

Stream: general

Topic: Definition without body


view this post on Zulip 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.

view this post on Zulip Alex J. Best (Dec 03 2020 at 04:00):

You could define the body as := sorry

view this post on Zulip Kenny Lau (Dec 03 2020 at 04:01):

or you can use constant

view this post on Zulip Kenny Lau (Dec 03 2020 at 04:01):

(which behaves exactly like axiom)

view this post on Zulip 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