Stream: math-comp users

Topic: negPf


view this post on Zulip Pierre Jouvelot (Aug 27 2023 at 19:01):

Why is this apply not doing the usual reflection thing, and is just a no-op? I must be missing something....

From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo b : b = false.
Proof.
Set Printing All.
apply/negPf.

view this post on Zulip Paolo Giarrusso (Aug 27 2023 at 21:10):

Googling leads to https://github.com/coq/coq/issues/10391 — I'm not sure what's going on, but the first example with move /negPf strongly implies that's related

view this post on Zulip Paolo Giarrusso (Aug 27 2023 at 21:12):

It seems https://github.com/math-comp/math-comp/issues/284#issuecomment-463204494 lists the actual answer, although I don't yet follow.

view this post on Zulip Pierre Jouvelot (Aug 28 2023 at 08:14):

@Pierre Roux Will do then, with pleasure :)

view this post on Zulip Notification Bot (Aug 28 2023 at 08:14):

Pierre Jouvelot has marked this topic as unresolved.


Last updated: Oct 13 2024 at 01:02 UTC