source: driver/extracted/extralib.ml

Last change on this file was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.6 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
30let eq_rect_Type0_r a p x0 =
31  Logic.eq_rect_r a x0 p
32
33(** val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
34let eq_rect_r2 a x x0 =
35  (fun _ h -> h) __ x0
36
37(** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
38let eq_rect_Type2_r a p x0 =
39  eq_rect_r2 a x0 p
40
41(** val dec_bounded_forall :
42    (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
43let dec_bounded_forall hP_dec k =
44  Nat.nat_rect_Type0 (Types.Inl __) (fun k0 hind ->
45    match hind with
46    | Types.Inl _ ->
47      (match hP_dec k0 with
48       | Types.Inl _ -> Types.Inl __
49       | Types.Inr _ -> Types.Inr __)
50    | Types.Inr _ -> Types.Inr __) k
51
52(** val dec_bounded_exists :
53    (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
54let dec_bounded_exists hP_dec k =
55  Nat.nat_rect_Type0 (Types.Inr __) (fun k0 hind ->
56    match hind with
57    | Types.Inl _ -> Types.Inl __
58    | Types.Inr _ ->
59      (match hP_dec k0 with
60       | Types.Inl _ -> Types.Inl __
61       | Types.Inr _ -> Types.Inr __)) k
62
63(** val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
64let dec_true f h =
65  match f with
66  | Types.Inl x -> h x
67  | Types.Inr _ -> assert false (* absurd case *)
68
69(** val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
70let dec_false f h =
71  match f with
72  | Types.Inl _ -> assert false (* absurd case *)
73  | Types.Inr x -> h x
74
Note: See TracBrowser for help on using the repository browser.