dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

More cleaning

This commit is contained in:
Niels 2017-08-07 16:57:21 +02:00
parent 1e373364b2
commit 8c10ab1c0c
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
FiniteSets/fsets/operations_decidable.v
View File

@ -7,7 +7,7 @@ Section decidable_A.
Context {A_deceq : DecidablePaths A}. Context {A_deceq : DecidablePaths A}.
Context `{Univalence}. Context `{Univalence}.
Global Instance isIn_decidable : forall (a : A) (X : FSet A), Decidable (isIn a X). Global Instance isIn_decidable : forall (a : A) (X : FSet A), Decidable (a ∈ X).
Proof. Proof.
intros a. intros a.
hinduction ; try (intros ; apply path_ishprop). hinduction ; try (intros ; apply path_ishprop).
@ -24,12 +24,12 @@ Section decidable_A.
Defined. Defined.
Definition isIn_b (a : A) (X : FSet A) := Definition isIn_b (a : A) (X : FSet A) :=
match dec (isIn a X) with match dec (a ∈ X) with
| inl _ => true | inl _ => true
| inr _ => false | inr _ => false
end. end.
Global Instance subset_decidable : forall (X Y : FSet A), Decidable (subset X Y). Global Instance subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y).
Proof. Proof.
hinduction ; try (intros ; apply path_ishprop). hinduction ; try (intros ; apply path_ishprop).
- intro ; apply _. - intro ; apply _.
@ -38,7 +38,7 @@ Section decidable_A.
Defined. Defined.
Definition subset_b (X Y : FSet A) := Definition subset_b (X Y : FSet A) :=
match dec (subset X Y) with match dec (X ⊆ Y) with
| inl _ => true | inl _ => true
| inr _ => false | inr _ => false
end. end.