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`

?

Program is whole-command only

If it helps: you might be able to achieve what you want without Program, using either l`tac:(tactic)`

or tricks like https://github.com/bedrocksystems/BRiCk/blob/53d812ff5ab56924e01283a52d854e403d16b57a/theories/prelude/fin.v#L57-L62

Last updated: Jun 16 2024 at 01:42 UTC