Skip to content
Snippets Groups Projects
Commit ffb7f0cc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Minor beautification.

parent 8d0efe8e
Branches
Tags
No related merge requests found
...@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) := ...@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
Fin.of_nat_lt (encode_lt_card x). Fin.of_nat_lt (encode_lt_card x).
Program Definition decode_fin `{Finite A} (i : fin (card A)) : A := Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
match Some_dec (decode_nat i) return _ with match Some_dec (decode_nat i) return _ with
| inleft (exist _ x _) => x | inright _ => _ | inleft (x _) => x | inright _ => _
end. end.
Next Obligation. Next Obligation.
intros A ?? i ?; exfalso. intros A ?? i ?; exfalso.
......
...@@ -40,10 +40,10 @@ Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f. ...@@ -40,10 +40,10 @@ Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _ / : assert. Arguments hlam _ _ _ _ _ / : assert.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B := Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs := (fix go {As} xs :=
match xs in hlist As return himpl As B B with match xs in hlist As return himpl As B B with
| hnil => λ f, f | hnil => λ f, f
| @hcons A As x xs => λ f, go As xs (f x) | hcons x xs => λ f, go xs (f x)
end) _ xs f. end) _ xs f.
Coercion hcurry : himpl >-> Funclass. Coercion hcurry : himpl >-> Funclass.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment