The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Sounds like that would bloat the search space of CS. In this case is obvious, but how do you foresee if you need some coercion (and which one!)?

Written from mobile. Excuse my limited communication.

On Sat, Feb 29, 2020, 11:39 AM Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

Is there a way to get canonical structures and coercions to work together? Here's my toy example:

Structure EX : Type :=
{ t :> Type
; GET : t -> Prop }.

Definition foo {e : EX} := e.(GET).

Canonical Structure TrueEX : EX :=
  {| GET := fun _ : bool => true |}.

Definition to_bool (n : nat) :=
  match n with
  | 0 => false
  | _ => true
  end.

Coercion to_bool : nat >-> bool.

Check (foo true). (* works great! *)
Check (foo 1).    (* fails *)

Intuitively, I would expect the term [@foo boolEX (to_bool 1)] but instead I get a type error "the term 1 has type nat while it is expected to have type EX".

Is there some way to make this work without making instances for, e.g. [natEX], which is the composition of [to_bool] and [foo]?

Thanks.

--

gregory malecha

gmalecha.github.io