initial commit

.gitignore

@@ -0,0 +1 @@
+_build/

bin/dune

@@ -0,0 +1,4 @@
+(executable
+ (public_name proof_checker)
+ (name main)
+ (libraries proof_checker))

bin/main.ml

@@ -0,0 +1 @@
+let () = print_endline "Hi"

dune-project

@@ -0,0 +1,26 @@
+(lang dune 3.16)
+
+(name proof_checker)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name proof_checker)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune)
+ (tags
+  (topics "to describe" your project)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html

lib/dune

@@ -0,0 +1,2 @@
+(library
+ (name proof_checker))

lib/formula.ml

@@ -0,0 +1,11 @@
+type t =
+    | Relation of string * Term.t list
+    | Equal of Term.t * Term.t
+    | Bottom
+    | Neg of t
+    | Conj of t * t
+    | Disj of t * t
+    | Impl of t * t
+    | Iff of t * t
+    | Forall of t
+    | Exists of t

lib/formula.mli

@@ -0,0 +1,11 @@
+type t =
+    | Relation of string * Term.t list
+    | Equal of Term.t * Term.t
+    | Bottom
+    | Neg of t
+    | Conj of t * t
+    | Disj of t * t
+    | Impl of t * t
+    | Iff of t * t
+    | Forall of t
+    | Exists of t

lib/term.ml

@@ -0,0 +1,5 @@
+type t =
+    | Var of int
+    | Const of string
+    | Free of string
+    | Function of string * t list

lib/term.mli

@@ -0,0 +1,5 @@
+type t =
+    | Var of int
+    | Const of string
+    | Free of string
+    | Function of string * t list

proof_checker.opam

@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A short synopsis"
+description: "A longer description"
+maintainer: ["Maintainer Name"]
+authors: ["Author Name"]
+license: "LICENSE"
+tags: ["topics" "to describe" "your" "project"]
+homepage: "https://github.com/username/reponame"
+doc: "https://url/to/documentation"
+bug-reports: "https://github.com/username/reponame/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.16"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/username/reponame.git"

test/dune

@@ -0,0 +1,2 @@
+(test
+ (name test_proof_checker))