(* Check non-error failure in case of unsupported decidability scheme *)
Local Set Decidable Equality Schemes.
Inductive a := A with b := B.
(* But fails with error if explicitly asked for the scheme *)
Fail Scheme Equality for a.
| Messung V0.5 in Prozent |
|---|
| | | |
[Dauer der Verarbeitung: 0.12 Sekunden, vorverarbeitet 2026-09-29]
