Skip to main content
Proof Assistants Beta

Return to Question

deleted 8 characters in body
Source Link
taylor.2317
taylor.2317
  • 1.3k
  • 8
  • 36

SayIf I have onehad a module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

NowAnd in another file, B.v, I havehad:

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred. 
How tocould I let Coq know I always want abt to be @abt 𝒳 in B.v? The The intent is to avoid explicitly specifying them using @.

Thanks.

Say I have one module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

Now in another file B.v, I have

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred. How to let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

Thanks.

If I had a module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

And in another file, B.v, I had:

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred. 
How could I let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

minor update
Source Link
lyfeng
lyfeng
  • 167
  • 6

Say I have one module with implicit arguments declared as follows in file A.v:

Section A.
  Context {A B C𝒳 : Set}.
  DefinitionInductive somedef1abt ...
:= Abt_leaf Definition(x somedef2: ..𝒳) | Abt_node.
End A.

Now in another file B.v, I have defined

DefinitionRequire Import A.
Definition 𝒳 := nat.
DefinitionInductive Btyp := natTpe_num | Typ_str.
Definition Ctyp_to_abt (t : typ) : abt (* @abt 𝒳 *) := stringAbt_node.

Then, sometimes theThe implicit arguments in somedef1abt, when defining somedef2typ_of_abt... can't be inferred. How to let Coq know I always want argument A to be A, argument Babt to be B@abt 𝒳, etc in B.v? The intent is to avoid explicitly specifying them using @.

Thanks.

Say I have one module with implicit arguments declared as follows:

Section A.
  Context {A B C : Set}.
  Definition somedef1 ...
  Definition somedef2 ...
End A.

Now in another file, I have defined

Definition A := nat.
Definition B := nat.
Definition C := string.

Then, sometimes the implicit arguments in somedef1, somedef2... can't be inferred. How to let Coq know I always want argument A to be A, argument B to be B, etc. The intent is to avoid explicitly specifying them using @.

Thanks.

Say I have one module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

Now in another file B.v, I have

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred. How to let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

Thanks.

Source Link
lyfeng
lyfeng
  • 167
  • 6

How to set defaults for implicit arguments when they can't be inferred?

Say I have one module with implicit arguments declared as follows:

Section A.
  Context {A B C : Set}.
  Definition somedef1 ...
  Definition somedef2 ...
End A.

Now in another file, I have defined

Definition A := nat.
Definition B := nat.
Definition C := string.

Then, sometimes the implicit arguments in somedef1, somedef2... can't be inferred. How to let Coq know I always want argument A to be A, argument B to be B, etc. The intent is to avoid explicitly specifying them using @.

Thanks.