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.
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
Thank you!
o wow, Enrico, quite interesting book! I added to my read list. Thanks for the book!
Thanks to the both authors.
Last updated: Oct 13 2024 at 01:02 UTC