Skip to content
Snippets Groups Projects
Commit cef729e8 authored by Janno's avatar Janno
Browse files

remove unneeded, loopy uncurry decision instance

parent 6ce40f46
No related branches found
No related tags found
No related merge requests found
......@@ -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
end.
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).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment