Stream: Coq users

Topic: ✔ turn off coercions

view this post on Zulip Andrey Klaus (Dec 03 2021 at 08:49):

Hello everybody.
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).

Here nat_of_bool was applied. How can I have fail the Check consn true (consn false niln).?

view this post on Zulip Ana de Almeida Borges (Dec 03 2021 at 09:19):

A feature was recently merged to avoid importing coercions. Other than that I'm not aware of a way to turn them off.

view this post on Zulip Andrey Klaus (Dec 03 2021 at 09:29):

Oh, cool. Thank you, Ana. I thought I've missed it.

view this post on Zulip Notification Bot (Dec 03 2021 at 09:29):

Andrey Klaus has marked this topic as resolved.

Last updated: Apr 18 2024 at 07:02 UTC