source: extracted/extra_bool.ml @ 2746

Last change on this file since 2746 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 463 bytes
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13open Bool
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open Nat
22
23open Types
24
25open List
26
27open Util
28
29(** val if_elim :
30    Bool.bool -> 'a1 -> 'a1 -> (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
31let if_elim clearme e1 e2 x x0 =
32  (match clearme with
33   | Bool.True -> (fun e3 e4 _ auto auto' -> auto __)
34   | Bool.False -> (fun e3 e4 _ auto auto' -> auto' __)) e1 e2 __ x x0
35
Note: See TracBrowser for help on using the repository browser.