Stream: Coq users

Topic: Admitted for defintions


view this post on Zulip Callan McGill (Jan 30 2022 at 03:25):

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

view this post on Zulip Paolo Giarrusso (Jan 30 2022 at 03:35):

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.

view this post on Zulip Li-yao (Jan 30 2022 at 05:30):

Another way is to define an Axiom todo : forall {A}, A. Then you can write Definition i : nat := todo. in a single command.

view this post on Zulip Gaëtan Gilbert (Jan 30 2022 at 11:29):

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.

view this post on Zulip Gaëtan Gilbert (Jan 30 2022 at 11:30):

for Instance there's Declare Instance

view this post on Zulip Ali Caglayan (Jan 30 2022 at 12:04):

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?)

view this post on Zulip Gaëtan Gilbert (Jan 30 2022 at 12:05):

Axiom foo : forall {x:T}, ... should work fine

view this post on Zulip Gaëtan Gilbert (Jan 30 2022 at 12:07):

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