diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-01 14:16:25 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-01 14:16:34 -0400 |
| commit | 85e8e6c92ec2d9d5f565353707711eeccecb8b8e (patch) | |
| tree | f6f726b99bbcef477b61816682ea68235043192b /src/Util/IdfunWithAlt.v | |
| parent | 2f94ae453564764b530b11ae0a6533d973c0f5cd (diff) | |
Add cps versions of id_with_alt
Diffstat (limited to 'src/Util/IdfunWithAlt.v')
| -rw-r--r-- | src/Util/IdfunWithAlt.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Util/IdfunWithAlt.v b/src/Util/IdfunWithAlt.v index 9754c5b24..09bb2ca76 100644 --- a/src/Util/IdfunWithAlt.v +++ b/src/Util/IdfunWithAlt.v @@ -34,8 +34,7 @@ Definition id_tuple_with_alt {A n} | O => id_with_alt | S n' => id_tuple'_with_alt end. -Fixpoint id_tuple_with_alt_proof {A n} - {struct n} +Definition id_tuple_with_alt_proof {A n} : forall (value value_for_alt : tuple A n) {pf : value = value_for_alt}, tuple A n := match n with |