Stream: Coq users

Topic: ssreflect how bool value true can became Prop?


view this post on Zulip Andrey Klaus (Apr 03 2021 at 17:07):

well, quite simple code below can not be compiled (which is correct because bool value true is not from Prop)

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

Inductive test : forall a: Prop, Prop :=
| testconstr : test true.

Print test.

but when I add From mathcomp Require Import ssrbool. it compiles. And Check true. still reports true : bool.
Could anybody give me a small explanation about what is going on? Or a link where to read about it. Or both, if possible :)

From mathcomp Require Import ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive test : forall a: Prop, Prop :=
| testconstr : test true.

Print test.

view this post on Zulip Enrico Tassi (Apr 03 2021 at 17:25):

There is an automatic cast from bool to Prop called is_true. Set Printing Coercions will show it. See https://zenodo.org/record/4457887#.YGikvRKxW8Q page 112

view this post on Zulip Andrey Klaus (Apr 03 2021 at 18:05):

Thank you!

view this post on Zulip Andrey Klaus (Apr 03 2021 at 19:59):

o wow, Enrico, quite interesting book! I added to my read list. Thanks for the book!

view this post on Zulip Andrey Klaus (Apr 03 2021 at 20:11):

Thanks to the both authors.


Last updated: Feb 08 2023 at 23:03 UTC