Stream: Coq users

Topic: ✔ Q on coercions defined in modules


view this post on Zulip Gaëtan Gilbert (Jan 12 2024 at 18:31):

Import(coercions) module.

view this post on Zulip Julio Di Egidio (Jan 12 2024 at 18:42):

Thanks, wonderful, it even works with records... :)

Module PosInt.

  Structure T : Set :=
  {
    value : nat ;
    value_prop : 1 <= value ;
    value_to_nat :> nat := value ;
  }.

  Definition min : T :=
  {|
    value := 1 ;
    value_prop := le_n _;
  |}.

  Check min : nat.

End PosInt.

Fail Check PosInt.min : nat.

Import(coercions) PosInt.

Check PosInt.min : nat.

view this post on Zulip Notification Bot (Jan 12 2024 at 18:45):

Julio Di Egidio has marked this topic as resolved.


Last updated: Jun 23 2024 at 05:02 UTC