New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Give a name derived from the name of the type to dependent variables #113

Merged

proux01 merged 1 commit into coq-community:master from herbelin:master+naming-depending-variables

Aug 28, 2023

Contributor

herbelin commented Aug 6, 2023

This PR ensures that arguments of parametricity predicates/relations have a "nice" name. E.g., before:

Parametricity nat.
Print nat_R.
(*
Inductive nat_R : nat -> nat -> Set :=
    nat_R_O_R : nat_R 0 0
  | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0).
*)

with the PR:

Parametricity nat.
Print nat_R.
(*
Inductive nat_R : nat -> nat -> Set :=
    nat_R_O_R : nat_R 0 0
  | nat_R_S_R : forall n₁ n₂ : nat, nat_R n₁ n₂ -> nat_R (S n₁) (S n₂).
*)


          Give a name derived from the name of the type to dependent variables.

ff8df62

proux01 merged commit 074ba78 into coq-community:master

1 check passed

Collaborator

proux01 commented Aug 28, 2023

Nice, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet