blob: 10a6bc3d6833d76d8d5e51ee63fe68df06574f74 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Entry point for this web application *)
(* open Chadprover.Types *)
open Chadprover.To_string
(* open Chadprover.Lib_utils *)
open Chadprover.Lexing.Lexer
open Chadprover.Parsing.Parser
(* open Chadprover.Satisfiability.Satisfiable *)
let () =
let lex_result = lex "(p > (q > (p > p)))" in (* "a & b & c = z > x & y | c" *)
let parse_result = parse lex_result in
let proof = Chadprover.Sequent_calculus.Sequent_proof.prove_sequent (Seq([], [parse_result])) in
print string_of_stree proof
let () = Api.Startapp.startapp ()
|
