Hi all. I’m trying to define a record type using the dependent Inductive types dep_T
and dep_TT
. However when I try to construct the record type Huu
, it is not able to infer the dependency of dep_T _ _
, which is the type of get_huu
. What I hope to achieve is, given a term, say p1
, and with a proof term c1 : dep_TT
, it is able to infer that get_huu
is p2
and hence fill the placeholders with b c
respectively.
But I get the error:
Cannot infer this placeholder of type
"Tings" in environment:
Huu : forall n m : Tings, dep_T n m -> Type
n, m : Tings
x : dep_T n m
Here’s my code:
Inductive Tings := a | b | c | d.
Inductive dep_T : Tings -> Tings -> Type :=
| p1 : dep_T a b
| p2 : dep_T b c
| p3 : dep_T c d.
Inductive dep_TT : forall {w x y z : Tings}, (dep_T w x) ->
(dep_T y z) -> Type :=
| c1 : dep_TT p1 p2
| c2 : dep_TT p2 p3.
Record Huu {n m : Tings}(x : dep_T n m) :=
mk_huu { get_huu :> dep_T _ _; _ : dep_TT x get_huu}.