Is there any equivalent of Admitted for defintions (i.e. in gallina) or is it better to just change to proof mode?

Just proof mode AFAICT. I tried `ltac:(admit).`

but it doesn't work (which makes sense), nor does it save much.

```
Fail Definition i : nat := ltac:(admit).
Definition i : nat. Proof. Admitted.
```

Another way is to define an `Axiom todo : forall {A}, A.`

Then you can write `Definition i : nat := todo.`

in a single command.

Is there any equivalent of Admitted for defintions (i.e. in gallina) or is it better to just change to proof mode?

Axiom and aliases (Parameter)

`Definition i : nat. Proof. Admitted.`

This is equivalent to `Axiom i : nat.`

for Instance there's Declare Instance

Sometimes Admitted is easier to use however since you can also declare arguments as implicit. Something you cannot do with axiom without using Arguments later. (Why can't we do that actually?)

`Axiom foo : forall {x:T}, ...`

should work fine

we can't use `Axiom foo arg : type`

because Axiom thinks you're defining 2 axioms `foo`

and `arg`

TBH I'm not sure when that's useful, maybe we should deprecate multiple axioms in 1 command so we can reassign the syntax

Last updated: Jun 16 2024 at 04:03 UTC