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: Mar 28 2024 at 23:01 UTC