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

Possible Type in Section 6.10 Ad-hoc polymorphism #123

Open

czhang03 opened this issue Jun 8, 2021 · 0 comments

czhang03 commented Jun 8, 2021 •

edited

Loading

Here is the code from the book

Inductive phantom (T : Type) (p : T) := Phantom.

Definition set_of (T : eqType) (_ : phantom Type (Equality.sort T)) := seq T.
Notation "{ 'set' T }" := (set_of _ (Phantom Type T))
    (at level 0, format "{ ’set’  T }") : type_scope.

Since the book recommends the setting Set Implicit Arguments. which will make many arguments here implicit, therefore this code will not work

Here is a version that write out all the argument explicitly, which will pass the type checking

Inductive phantom (T : Type) (p : T) := Phantom.

Definition set_of (T : eqType) (_ : @phantom Type (Equality.sort T)) := seq T.
Notation "{ 'set' T }" := (@set_of _ (@Phantom Type T))
    (at level 0, format "{ 'set' T }") : type_scope.

(*Some examples*)
Check {set nat}.
Check [:: 1]: {set nat}.

The text was updated successfully, but these errors were encountered:

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