When I do not need coercion which I imported among other things, how can I turn it off?
in example I have
From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Inductive listn : Set := niln | consn (hd : nat) (tl : listn). Check consn true (consn false niln).
nat_of_bool was applied. How can I have fail the
Check consn true (consn false niln).?
A feature was recently merged to avoid importing coercions. Other than that I'm not aware of a way to turn them off.
Oh, cool. Thank you, Ana. I thought I've missed it.
Andrey Klaus has marked this topic as resolved.
Last updated: Feb 01 2023 at 13:03 UTC