Currently, the True and False constant circuits defined in Expr.v mask the definitions of True and False in Coq's core logic, meaning that if Expr.v is imported then you have to write Logic.True and Logic.False. It's a bit annoying and makes specifications/invariants/proof states less readable. (Some Coq IDE setups, including mine, display True and False as unicode logical symbols, which makes circuits less readable as well.)
Currently, the
TrueandFalseconstant circuits defined inExpr.vmask the definitions ofTrueandFalsein Coq's core logic, meaning that ifExpr.vis imported then you have to writeLogic.TrueandLogic.False. It's a bit annoying and makes specifications/invariants/proof states less readable. (Some Coq IDE setups, including mine, displayTrueandFalseas unicode logical symbols, which makes circuits less readable as well.)Are these names a suitable alternative?