blob: 295b7cd9f5679f42bf97a8abf2f2729bcb55d1b5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* Revealed a missing re-consideration of postponed problems *)
Module A.
Inductive flat_type := Unit | Prod (A B : flat_type).
Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
-> Type :=
| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
Inductive op : flat_type -> flat_type -> Type := .
Arguments Op {_ _ _ _} _ _.
Definition bound_op {var}
{src2 dst2}
(opc2 : op src2 dst2)
: forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2
:= match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end.
End A.
(* A shorter variant *)
Module B.
Inductive exprf (op : unit -> Type) : Type :=
| A : exprf op
| Op tR (opc : op tR) (args : exprf op) : exprf op.
Inductive op : unit -> Type := .
Definition bound_op (dst2 : unit) (opc2 : op dst2)
: forall (args2 : exprf op), Op op dst2 opc2 args2 = A op
:= match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end.
End B.
|
