Unsafe proofs

Stream: lean4

[Calvin Lee]

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

[Reid Barton]

sorry?

[Calvin Lee]

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