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
27
|
Require Coq.Program.Wf.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Inductive PolyType (R: Set): Set :=
| prt_leading: PolyType R.
Definition poly_deg {R: Set} (p: PolyType R): nat.
Admitted.
Definition RootExtensionType {F: Set} (p: PolyType F) (Hp: p <> p): Set.
Admitted.
Program Fixpoint SplittingExtensionType {K: Set} (p: PolyType K) {measure (poly_deg p)}: Set :=
match p with
| prt_leading _ => SplittingExtensionType (_: PolyType (RootExtensionType p _))
end.
Next Obligation.
Admitted.
Next Obligation.
admit.
Defined. (* anomaly "in Univ.repr: Universe Top.3 undefined." fixed by #18642 *)
Next Obligation.
Admitted.
Next Obligation.
Admitted.
|
