Skip to content

Proof mode support for monotonous predicates.

Jacques-Henri Jourdan requested to merge jh/bi_morphism into janno/monfun

Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.

Edited by Jacques-Henri Jourdan

Merge request reports