Zulip Chat Archive

Stream: lean4

Topic: Unsafe proofs


view this post on Zulip Calvin Lee (Jan 29 2021 at 00:29):

Is there any way to "generate" proofs in unsafe functions easily? e.g. just create an inhabitant of some {a : Prop}

view this post on Zulip Reid Barton (Jan 29 2021 at 00:35):

sorry?

view this post on Zulip Calvin Lee (Jan 29 2021 at 00:36):

sorry will warning, which I don't really want
I think this is exactly what I'm looking for though (did some grepping around) https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L52


Last updated: May 18 2021 at 22:15 UTC