You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The decidability of the NoDup predicate (NoDup_dec) is defined with Qed instead of Defined, which makes it opaque and thus makes it impossible to compute with it.
For example, other proofs of decidability of list operations (e.g. in_dec or list_eq_dec) are defined as transparent.
The text was updated successfully, but these errors were encountered:
The decidability of the
NoDup
predicate (NoDup_dec
) is defined withQed
instead ofDefined
, which makes it opaque and thus makes it impossible to compute with it.For example, other proofs of decidability of list operations (e.g.
in_dec
orlist_eq_dec
) are defined as transparent.The text was updated successfully, but these errors were encountered: