Stream: Coq users

Topic: Notation for `Program`

view this post on Zulip Julin S (Jun 25 2022 at 10:46):

We can get away with providing holes for proof if we use Program in the case of

Program Example foo : {n:nat | n < 2} :=
  exist _ 1 _.

(because the proof is given by le_n applied on 2.)

Is it possible to have a notation like

Notation {{ n }} :=
    Program Example foo : {n:nat | n < 2} :=
      exist _ n _.

And is there a way to not have to make a name like foo?

view this post on Zulip Gaëtan Gilbert (Jun 25 2022 at 10:59):

Program is whole-command only

view this post on Zulip Paolo Giarrusso (Jun 25 2022 at 12:09):

If it helps: you might be able to achieve what you want without Program, using either ltac:(tactic) or tricks like https://github.com/bedrocksystems/BRiCk/blob/53d812ff5ab56924e01283a52d854e403d16b57a/theories/prelude/fin.v#L57-L62

Last updated: Apr 16 2024 at 14:02 UTC