# Create a definition using a proof script inside a proof script

**URL:** <https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954>\
**Category:** Using Rocq\
**Created:** [July 20, 2020, 9:58pm UTC](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954 "2020-07-20T21:58:24Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [July 20, 2020, 9:58pm UTC](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954/1 "2020-07-20T21:58:24Z")

</div>

In some proofs it might be necessary to define some constant using the proof mode. Which of the following variants would you prefer / find more elegant?

_Poll ([view on site](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954/1))_

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [July 20, 2020, 9:58pm UTC](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954/2 "2020-07-20T21:58:31Z")

</div>

The first two options result in the same proof term. The second option is a bit weird because `evar` is supposed to create a new evar, which is then immediatly unshelved.

In the last option, the new hypthesis will be `z := (the_definition : nat) : nat`, which is weird due to the redundant type casting.

IMO, the clearest syntax would be `unshelve epose (z : nat := _).`

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [July 20, 2020, 11:54pm UTC](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954/3 "2020-07-20T23:54:56Z")

</div>

I use a plain `assert`, usually, or `unshelve evar` if I need it to be transparent.

Related: [https://github.com/coq/coq/issues/3551](https://github.com/coq/coq/issues/3551)

---

<div class="post-metadata">

**Author:** ![kyod](https://avatars.discourse-cdn.com/v4/letter/k/73ab20/32.png) [@kyod](https://discourse.rocq-prover.org/u/kyod)\
**Post date:** [July 21, 2020, 7:38am UTC](https://discourse.rocq-prover.org/t/create-a-definition-using-a-proof-script-inside-a-proof-script/954/4 "2020-07-21T07:38:17Z")

</div>

You can also use `simple refine (let x : nat := _ in _).` with a similar effect, no ?