Skip to content

have solve_proper exploit OfeDiscrete and LeibnizEquiv

Ralf Jung requested to merge ralf/solve-proper-subrelation into master

This makes solve_proper handle goals like NonExpansive (λ x, ⌜a = x⌝). Depends on stdpp!495 (merged).

Edited by Ralf Jung

Merge request reports