The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Definition poly_out x :=
  match x return match x with | O => unit | _ => nat end with
  | O => tt
  | S _ => 0
  end
.

Definition poly_in i (x : match i with | 0 => unit | _ => nat end) :=
  match i as j return (match j with | 0 => unit | _ => nat end -> nat) with
  | 0 => fun u =>
    match u with
    | tt => 0
    end
  | _ => fun n =>
    match n with
    | 0 => 1
    | _ => 2
    end
  end x
.

(*
Compute (fun j => poly_in j (poly_out j)).

The term "poly_out j" has type "match j with
                                | 0 => unit
                                | S _ => nat
                                end" while it is expected to have type
 "match j with
  | 0 => unit
  | S _ => nat
  end".

Is there a way to write that expression to make it type check?
What is it unhappy about?

I also found that Coq (8.3pl1) doesn't want to infer the value
for i in poly_in, so leaving it implicit doesn't work.

I realize that normally I would just declare a new tagged union type,
which would handle the tag i parameter automatically, but I wanted
to see what happens if I go this way.
*)

- -- 
*********************.************************************..|
**..*.*...*..**....**....*....**....***.**...*..***.......*.|
*..**.**...**.***...*...*..*.**..****...*...*.*.....**..*...|
.*..*..*.*..*.....******...*.*..*.*.**...*.**.*..*..***..*..|
...*.*..*..***..*.*****...*...*....****.....***.*...**..**..|
..*.....**..***.*.........*.*...*..**..**game*.....*........|
*....*..**..*.*.*.*..*.**.*..*..*..**..**of**......**.***...|
*.**.*..**..*.*.**.**..**.**.****..***life.**.****..*.****..|
**********************************************************..|
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAlCoKckACgkQxzVgPqtIcfsX5QCfYP3vdjrJvCFg+X51ardCgc4I
6PIAniT9tPcSiczmHWjhjnzlyyMX1lbS
=LZz5
-----END PGP SIGNATURE-----