search

math-comp / mcb

Mathematical Components (the Book)
Other
139 stars 25 forks source link

Possible Type in Section 6.10 Ad-hoc polymorphism #123

Open czhang03 opened 3 years ago

czhang03 commented 3 years ago

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}.