Commit 46648f14 authored by Janno's avatar Janno

remove unneeded, loopy uncurry decision instance

parent 352f1865
Pipeline #711 passed with stage
......@@ -180,8 +180,6 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
match p as p return Decision (curry P p) with
| (x,y) => P_dec x y
Instance uncurry_dec `(P_dec : (p : A * B), Decision (P p)) x y :
Decision (uncurry P x y) := P_dec (x,y).
Instance sig_eq_dec `(P : A Prop) `{ x, ProofIrrel (P x)}
`{ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment