Stream: math-comp users

Topic: ✔ homo typechecking

Pierre Jouvelot (Mar 13 2022 at 18:06):

I seem to be unable to make this typecheck. What am I missing?

From mathcomp Require Import all_ssreflect.

Lemma foo (T : finType) (f : nat -> {set T}):
  {homo f : x y / x \subset y}.

Pierre Roux (Mar 13 2022 at 18:09):

maybe

  {homo f : x y / x <= y >-> x \subset y}.

Pierre Jouvelot (Mar 13 2022 at 18:14):

Indeed, thanks! These notations seemed to me to be expanding to the same result, but apparently not ;)

Pierre Jouvelot (Mar 13 2022 at 18:17):

Ah, no! stupid mistake on my part. Sorry for the disturbance. Thanks.

Notification Bot (Mar 13 2022 at 18:42):

Pierre Roux has marked this topic as resolved.

Last updated: Feb 08 2023 at 07:02 UTC