Skip to content
GitLab

have solve_proper exploit OfeDiscrete and LeibnizEquiv

Merged 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