tests the computes non-uniform parameter
Load non_uniform.
Compute (countOfCtor 1 100 (tApp (tRel 1) (tRel 0))).
Compute (countOfCtor 1 100 (tApp (tRel 100) (tApp (tRel 1) (tRel 0)))).
Compute (countOfCtor 1 100 (tApp (tVar "Not relevant"%string) (tApp (tRel 1) (tRel 0)))).
Compute (countOfCtor 1 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tRel 1) (tRel 0)))).
(* Compute (countOfCtor 1 1 (tApp (tApp (tRel 1) (tRel 0)) (tVar "N"*)
Compute (countOfCtor 2 2 (tApp (tApp (tRel 2) (tRel 1)) (tVar "N"%string))).
Compute (countOfCtor 2 100 (tApp (tApp (tRel 2) (tRel 1)) (tVar "N"%string))).
Compute (countOfCtor 2 100 (tApp (tApp (tRel 2) (tRel 0)) (tVar "N"%string))).
Compute (countOfCtor 2 100 (tApp (tApp (tRel 2) (tRel 1)) (tRel 0))).
Compute (countOfCtor 2 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 2) (tRel 1)) (tRel 0)))).
Compute (countOfCtor 2 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 2) (tRel 42)) (tRel 0)))).
Compute (countOfCtor 2 2 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 2) (tRel 42)) (tRel 1)))). (* Problem *)
Compute (countOfCtor 2 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 2) (tRel 1)) (tRel 42)))).
Compute (countOfCtor 1 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 1) (tRel 42)) (tRel 42)))).
Compute (countOfCtor 1 100 (tApp
(tInd {| inductive_mind := "Coq.Init.Datatypes.list"; inductive_ind := 0 |} [])
(tApp (tApp (tRel 1) (tVar "N"%string)) (tVar "N"%string)))).
Compute (countOfCtor 1 100
(tApp
(tInd
{|
inductive_mind := "Coq.Init.Datatypes.list";
inductive_ind := 0 |} [])
(tApp(tApp (tRel 1)
(* (tApp *)
(* (tConstruct *)
(* {| *)
(* inductive_mind := "Coq.Init.Datatypes.nat"; *)
(* inductive_ind := 0 |} 1 ) (tRel 0)) *)
(tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} 0 [])
)
(tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} 0 [])
))
).
MetaCoq Run (getP <% nat %>). (* 0 *)
MetaCoq Run (getP <% list %>). (* 1 *)
MetaCoq Run (getP <% VectorDef.t %>). (* 1 *)
MetaCoq Run (getP <% le %>). (* 1 *)
MetaCoq Run (getP <% Acc %>). (* 2 *)
Definition t1 := Ast.tProd (nNamed "n"%string)
(Ast.tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} [])
(Ast.tApp (Ast.tRel 1)
[Ast.tRel 0; Ast.tRel 0]).
Definition t2 := Ast.tProd (nNamed "n"%string)
(Ast.tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} [])
(Ast.tProd (nNamed "m"%string)
(Ast.tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} [])
(Ast.tProd nAnon
(Ast.tApp
(Ast.tRel 2)
[Ast.tRel 1; Ast.tRel 0])
(Ast.tApp
(Ast.tRel 3)
[Ast.tRel 2;
Ast.tApp
(Ast.tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} 1 [])
[
Ast.tRel 1]]))).
From MetaCoq.PCUIC Require Import TemplateToPCUIC.
Compute (countOfCtor 0 2 (trans t1)).
Compute (countOfCtor 0 2 (trans t2)).
MetaCoq Run (tmQuoteInductive ("le"%string) >>= tmPrint).
Definition vt1 :=
Ast.tProd (nNamed "A"%string)
(Ast.tSort
(Universe.from_kernel_repr
(Level.Level
"Coq.Vectors.VectorDef.4",
false) []))
(Ast.tApp (Ast.tRel 1)
[Ast.tRel 0;
Ast.tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} 0 []]).
Definition vt2 :=
Ast.tProd (nNamed "A"%string)
(Ast.tSort
(Universe.from_kernel_repr
(Level.Level
"Coq.Vectors.VectorDef.4",
false) []))
(Ast.tProd (nNamed "h"%string)
(Ast.tRel 0)
(Ast.tProd
(nNamed "n"%string)
(Ast.tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} [])
(Ast.tProd nAnon
(Ast.tApp
(Ast.tRel 3)
[Ast.tRel 2; Ast.tRel 0])
(Ast.tApp
(Ast.tRel 4)
[
Ast.tRel 3;
Ast.tApp
(Ast.tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} 1 [])
[Ast.tRel 1]])))).
MetaCoq Run (tmQuoteInductive ("VectorDef.t"%string) >>= tmPrint).
From MetaCoq.PCUIC Require Import TemplateToPCUIC.
Compute (countOfCtor 0 2 (trans vt1)).
Compute (countOfCtor 0 2 (trans vt2)).
Print Coq.Init.Logic.eq_refl.
Inductive dep (X:Type) : nat -> forall (x:X), x=x -> Prop :=
| dep0 y : dep X 0 y (@Coq.Init.Logic.eq_refl _ y).
Inductive G (f:nat->bool) : nat -> Prop :=
GI : forall n, (f n = false -> G f (S n)) -> G f n.
Inductive G3 (f:nat->bool) (n:nat) : Prop :=
G3I : (f n = false -> G3 f (S n)) -> G3 f n.
Inductive G2 (f:nat->bool) : nat -> Prop :=
G2I1 : forall n, (f n = false -> G2 f (S n)) -> (f n = true -> G2 f (S (S n))) -> G2 f n
| G2I2 : forall n, (f n = false -> G2 f (S n)) -> G2 f n.
MetaCoq Run (getP <% dep %>).
MetaCoq Run (getP <% G %>).
MetaCoq Run (getP <% G3 %>).
MetaCoq Run (getP <% G2 %>).
Inductive roseTreePI8 (n : nat) : nat -> Set := treePI8 : list (roseTreePI8 (S n) 0) -> roseTreePI8 n 1.
MetaCoq Run (tmQuoteInductive ("roseTreePI8"%string) >>= tmPrint).
MetaCoq Run (getP <% roseTreePI8 %>).