nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma
normale. Spostare la small_delta_step.
+
+@ tra universi senza duplicati
-------
?1 = t
(?1,?2)::(?2,t)::subst
String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
;;
+let universes = ref [];;
+
let add_constraint strict a b =
match a,b with
| [false,a2],[false,b2] ->
if le_path_uri [] (not strict) b2 a2 then
(raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2
^ " to:\n" ^ pp_constraints ()))));
+ universes := a2 :: b2 ::
+ List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
le_constraints := (strict,a2,b2) :: !le_constraints)
| _ -> raise (BadConstraint
(lazy "trying to add a constraint on an inferred universe"))
;;
+let sup l =
+ match l with
+ | [false,_] -> Some l
+ | l ->
+ let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in
+ let solutions = List.fold_left bigger_than !universes l in
+ let rec aux = function
+ | [] -> None
+ | u :: tl ->
+ if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl
+ else Some [false,u]
+ in
+ aux solutions
+;;
+
+
+
let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
let set_typecheck_obj f =
if !already_set then
true -> strict check (<); false -> loose check (<=)
*)
val add_constraint: bool -> NCic.universe -> NCic.universe -> unit
+val sup : NCic.universe -> NCic.universe option
val pp_constraints: unit -> string
val get_checked_def:
nCicMetaSubst.cmx: nCicMetaSubst.cmi
nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi
nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi
-nCicRefiner.cmo: nCicRefiner.cmi
-nCicRefiner.cmx: nCicRefiner.cmi
+nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi
+nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi
in
prerr_endline "ranked....";
prerr_endline (NCicEnvironment.pp_constraints ());
+(*
+ let [_,type0_uri] = mk_type 0 in
+ let [_,type1_uri] = mk_type 1 in
+ let [_,type2_uri] = mk_type 2 in
+ prerr_endline
+ ("Min:" ^
+ (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with
+ | None -> "NO SUP"
+ | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]
+ (NCic.Sort (NCic.Type t))));
+*)
HExtlib.profiling_enabled := false;
List.iter (fun uu ->
let uu= OCic2NCic.nuri_of_ouri uu in
let rec aux metasenv subst context ind arity1 arity2 =
(*D*)inside 'S'; try let rc =
let arity1 = NCicReduction.whd ~subst context arity1 in
+ pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " ... " ^
+ NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nNEV:"^
+NCicPp.ppmetasenv ~subst metasenv
+));
match arity1 with
| C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
let metasenv, meta, _ =
- NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Typeless
+ NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type
in
let metasenv, subst =
try NCicUnification.unify metasenv subst context
- (C.Prod (name, so1, meta)) arity2
+ arity2 (C.Prod (name, so1, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
- (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+ (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
(NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
in
aux metasenv subst ((name, C.Decl so1)::context)
(mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
| C.Sort _ (* , t ==?== C.Prod _ *) ->
- let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Typeless in
+ let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
let metasenv, subst =
try NCicUnification.unify metasenv subst context
- (C.Prod ("_", ind, meta)) arity2
+ arity2 (C.Prod ("_", ind, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
- (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+ (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
(NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
in
(try NCicTypeChecker.check_allowed_sort_elimination
let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-(*
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
-*)
-let pp _ = ();;
+(* let pp _ = ();; *)
+
+let fix_sorts metasenv subst context meta t =
+ let rec aux () = function
+ | NCic.Sort (NCic.Type u) as orig ->
+ (match NCicEnvironment.sup u with
+ | None -> raise (fail_exc metasenv subst context meta t)
+ | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+ | NCic.Meta _ as orig -> orig
+ | t -> NCicUtils.map (fun _ _ -> ()) () aux t
+ in
+ aux () t
+;;
let rec beta_expand num test_eq_only swap metasenv subst context t arg =
let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
(* (*D*) in outside (); rc with exn -> outside (); raise exn *)
and instantiate test_eq_only metasenv subst context n lc t swap =
-(* (*D*) inside 'I'; try let rc = *)
+ (*D*) inside 'I'; try let rc =
let unify test_eq_only m s c t1 t2 =
if swap then unify test_eq_only m s c t2 t1
else unify test_eq_only m s c t1 t2
in
+ let fix_sorts t =
+ if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
+ else
+ NCic.Sort (NCic.Type (
+ match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
+ assert false))
+ in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
- let metasenv, subst =
+ let metasenv, subst, t =
match ty with
- | NCic.Implicit (`Typeof _) -> metasenv, subst
+ | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
| _ ->
- let lty = NCicSubstitution.subst_meta lc ty in
- let ty_t =
- try NCicTypeChecker.typeof ~subst ~metasenv context t
- with NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
- prerr_endline (Lazy.force msg);
- assert false
+ pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+ let t, ty_t =
+ try t, NCicTypeChecker.typeof ~subst ~metasenv context t
+ with NCicTypeChecker.TypeCheckerFailure _ ->
+ let ft = fix_sorts t in
+ if ft == t then assert false else
+ try
+ pp (lazy ("typeof: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ft));
+ ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
+ with NCicTypeChecker.TypeCheckerFailure msg ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
+ prerr_endline (Lazy.force msg);
+ assert false
in
+ let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy("On the types: " ^
NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
- unify test_eq_only metasenv subst context lty ty_t
+ let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
+ metasenv, subst, t
in
let (metasenv, subst), t =
try NCicMetaSubst.delift metasenv subst context n lc t
List.filter (fun (m,_) -> not (n = m)) metasenv
in
metasenv, subst
-(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
and unify test_eq_only metasenv subst context t1 t2 =
-(* (*D*) inside 'U'; try let rc = *)
+ (*D*) inside 'U'; try let rc =
let fo_unif test_eq_only metasenv subst t1 t2 =
-(* (*D*) inside 'F'; try let rc = *)
-(*
+ (*D*) inside 'F'; try let rc =
pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
NCicPp.ppterm ~metasenv ~subst ~context t2));
-*)
if t1 === t2 then
metasenv, subst
else
raise (uncert_exc metasenv subst context t1 t2))
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| _ -> raise (uncert_exc metasenv subst context t1 t2)
-(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
in
let height_of = function
| NCic.Const (Ref.Ref (_,Ref.Def h))
let rec unif_machines metasenv subst =
function
| ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
-(* (*D*) inside 'M'; try let rc = *)
+ (*D*) inside 'M'; try let rc =
(*
pp (lazy((if are_normal then "*" else " ") ^ " " ^
NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
unif_machines metasenv subst (small_delta_step m1 m2)
-(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
in
try fo_unif test_eq_only metasenv subst t1 t2
with UnificationFailure msg | Uncertain msg as exn ->
with
| UnificationFailure _ -> raise (UnificationFailure msg)
| Uncertain _ -> raise exn
-(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
;;
let unify =
ous_stuff :> ordered_uniform_space_;
ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
}.
-
+(*
definition Type_of_ordered_uniform_space : ordered_uniform_space → Type.
intro; compose ordered_set_OF_ordered_uniform_space with os_l.
apply (hos_carr (f o));
apply (hos_carr (f o));
qed.
-coercion Type_of_ordered_uniform_space.
coercion Type_of_ordered_uniform_space_dual.
-
+coercion Type_of_ordered_uniform_space.
+*)
definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set.
intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o);
qed.
[1: intros (U H); intro x; simplify;
cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm;
lapply (us_phi1 O w Gw x Hm) as IH;
- apply (restrict ? l r ??? Hwp IH); STOP
+ apply (restrict ? l r ??? Hwp IH);
|2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV;
cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv;
- cases (us_phi2 ??? Gu Gv) (w HW); cases HW (Gw Hw); clear HW;
- exists; [apply (λb:{[l,r]} square.w b)] split;
+ cases (us_phi2 O u v Gu Gv) (w HW); cases HW (Gw Hw); clear HW;
+ exists; [apply (λb:{[l,r]} squareB.w b)] split;
[1: unfold f; simplify; clearbody f;
exists; [apply w]; split; [assumption] intro b; simplify;
unfold segment_square_of_ordered_set_square;
cases b; intros; split; intros; assumption;
|2: intros 2 (x Hx); cases (Hw ? Hx); split;
- [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]]
+ [apply (restrict O l r ??? HuU H)|apply (restrict O l r ??? HvV H1);]]
|3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU;
- cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW;
- exists; [apply (λx:{[l,r]} square.w x)] split;
+ cases (us_phi3 O u Gu) (w HW); cases HW (Gw Hwu); clear HW;
+ exists; [apply (λx:{[l,r]} squareB.w x)] split;
[1: exists;[apply w];split;[assumption] intros; simplify; intro;
unfold segment_square_of_ordered_set_square;
cases b; intros; split; intro; assumption;
- |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu;
+ |2: intros 2 (x Hx); apply (restrict O l r ??? HuU); apply Hwu;
cases Hx (m Hm); exists[apply (\fst m)] apply Hm;]
|4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
- cases (us_phi4 ?? Gu x) (Hul Hur);
+ cases (us_phi4 O u Gu x) (Hul Hur);
split; intros;
- [1: lapply (invert_restriction_agreement ????? HuU) as Ra;
- apply (restrict ????? x Ra);
- apply Hul; apply (unrestrict ?????? HuU H);
- |2: apply (restrict ?????? HuU); apply Hur;
- apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]]
+ [1: lapply (invert_restriction_agreement O l r ?? HuU) as Ra;
+ apply (restrict O l r ?? x Ra);
+ apply Hul; apply (unrestrict O l r ??? HuU H);
+ |2: apply (restrict O l r ??? HuU); apply Hur;
+ apply (unrestrict O l r ??? (invert_restriction_agreement O l r ?? HuU) H);]]
|2: simplify; reflexivity;]
|2: simplify; unfold convex; intros;
cases H (u HU); cases HU (Gu HuU); clear HU H;
- lapply (ous_convex ?? Gu (bs_of_ss ? l r p) ? H2 (bs_of_ss ? l r y) H3) as Cu;
- [1: apply (unrestrict ?????? HuU); apply H1;
- |2: apply (restrict ?????? HuU Cu);]]
+ lapply (ous_convex ?? Gu p ? H2 y H3) as Cu;
+ [1: apply (unrestrict O l r ??? HuU); apply H1;
+ |2: apply (restrict O l r ??? HuU Cu);]]
qed.
interpretation "Ordered uniform space segment" 'segment_set a b =
alias symbol "pi1" = "exT \fst".
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
- ∀x:{[l,u]}.
- ∀a:sequence {[l,u]}.
- ⌊n,\fst (a n)⌋ uniform_converges (\fst x) →
+ ∀x:(segment_ordered_uniform_space O l u).
+ ∀a:sequence (segment_ordered_uniform_space O l u).
+ uniform_converge (segment_ordered_uniform_space O l u)
+ (mk_seq O (λn:nat.\fst (a n))) (\fst x) → True.
a uniform_converges x.
intros 8; cases H1; cases H2; clear H2 H1;
cases (H ? H3) (m Hm); exists [apply m]; intros;
+Z/times.ma Z/plus.ma nat/lt_arith.ma
list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
-Z/times.ma Z/plus.ma nat/lt_arith.ma
nat/factorial.ma nat/le_arith.ma
nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
nat/lt_arith.ma nat/div_and_mod.ma
nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
+nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma
-nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
Z/orders.ma Z/z.ma nat/orders.ma
datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma
-nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
logic/connectives2.ma higher_order_defs/relations.ma
+nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma
nat/o.ma nat/binomial.ma nat/sqrt.ma
-Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
-Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
+Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
nat/plus.ma nat/nat.ma
+Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
formal_topology/saturations_reductions.ma datatypes/subsets.ma
algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
datatypes/categories.ma logic/cprop_connectives.ma
nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
-higher_order_defs/ordering.ma logic/equality.ma
-nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
-Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma
+nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
+higher_order_defs/ordering.ma logic/equality.ma
datatypes/constructors.ma logic/equality.ma
+Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma
Z/compare.ma Z/orders.ma nat/compare.ma
-Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
+Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
-decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
-Q/ratio/ratio.ma Q/fraction/fraction.ma
datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
-nat/div_and_mod_diseq.ma nat/lt_arith.ma
nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
-technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
+Q/ratio/ratio.ma Q/fraction/fraction.ma
+nat/div_and_mod_diseq.ma nat/lt_arith.ma
+decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
logic/connectives.ma
+technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
datatypes/compare.ma
nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
nat/factorial2.ma nat/exp.ma nat/factorial.ma
nat/chebyshev_thm.ma nat/neper.ma
algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
-nat/gcd_properties1.ma nat/gcd.ma
demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
+nat/gcd_properties1.ma nat/gcd.ma
nat/minimization.ma nat/minus.ma
decidable_kit/fgraph.ma decidable_kit/fintype.ma
-formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma
formal_topology/relations.ma datatypes/subsets.ma
+formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma
Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
Z/plus.ma Z/z.ma nat/minus.ma
-Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
nat/minus.ma nat/compare.ma nat/le_arith.ma
-formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma
+nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
+Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
Z/z.ma datatypes/bool.ma nat/nat.ma
+formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma
decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
nat/map_iter_p.ma nat/count.ma nat/permutation.ma
-decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
+decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
nat/gcd.ma nat/lt_arith.ma nat/primes.ma
nat/factorization.ma nat/ord.ma
-decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
algebra/monoids.ma algebra/semigroups.ma
-logic/coimplication.ma logic/connectives.ma
demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
-higher_order_defs/functions.ma logic/equality.ma
+logic/coimplication.ma logic/connectives.ma
+decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
+higher_order_defs/functions.ma logic/equality.ma
algebra/semigroups.ma higher_order_defs/functions.ma
-Q/nat_fact/times.ma nat/factorization.ma
-nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
nat/sieve.ma list/sort.ma nat/primes.ma
+nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
+Q/nat_fact/times.ma nat/factorization.ma
nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
-higher_order_defs/relations.ma logic/connectives.ma
-nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
logic/cprop_connectives.ma logic/connectives.ma
+nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
+higher_order_defs/relations.ma logic/connectives.ma
demo/toolbox.ma logic/cprop_connectives.ma
-Q/inv.ma Q/q/q.ma Q/fraction/finv.ma Q/q.ma
demo/natural_deduction.ma
+Q/inv.ma Q/q/q.ma Q/fraction/finv.ma Q/q.ma
decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
-Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/nat.ma nat/factorization.ma
Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma
Q/q/qplus.ma nat/factorization.ma
+Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/nat.ma nat/factorization.ma
Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma
nat/nat.ma higher_order_defs/functions.ma
formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma
nat/chebyshev.ma nat/o.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma
+demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma
nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
nat/le_arith.ma nat/orders.ma nat/times.ma
-demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma
nat/times.ma nat/plus.ma
formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma
list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
-nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
+nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
projects / helm.git / commitdiff