diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-01 16:50:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-01 16:50:18 -0400 |
| commit | 8be5328b8771ee560922a0767d64b57268e40968 (patch) | |
| tree | cfbe505a7e0cd982d285b6249d2b1e6cdd8ff2a3 /src/Util/HList.v | |
| parent | 80a24b1d6215e8d240cc355bd4989f4aa6dcb33f (diff) | |
Change hlist implicit status
Diffstat (limited to 'src/Util/HList.v')
| -rw-r--r-- | src/Util/HList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index addb0e40d..8013e8b15 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -20,13 +20,13 @@ Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := end. (* tuple map *) -Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall ts : tuple' A n, hlist' F ts -> tuple' B n +Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall {ts : tuple' A n}, hlist' F ts -> tuple' B n := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with | 0 => fun ts v => f _ v | S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v)) end. Definition mapt {n A F B} (f : forall x : A, F x -> B) - : forall ts : tuple A n, hlist F ts -> tuple B n + : forall {ts : tuple A n}, hlist F ts -> tuple B n := match n return forall ts : tuple A n, hlist F ts -> tuple B n with | 0 => fun ts v => tt | S n' => @mapt' n' A F B f |