added man page

2 files changed, 97 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index 3abb97e..bb908a7 100644
--- a/Makefile
+++ b/Makefile
@@ -3,14 +3,16 @@ CFLAGS+= -Wshadow -Wstrict-prototypes -Wundef -Wpointer-arith
 CFLAGS+= -Wunreachable-code -Wformat=2 -g
 PREFIX ?= /usr
 BINDIR ?= ${PREFIX}/bin
+MANDIR = ${PREFIX}/share/man
 
 generate:
 	$(CC) -o operetta src/operetta.c src/proposition.c src/parse.c src/lexer.c src/eval.c src/console.c src/conio.c $(CFLAGS)
 
 install: operetta
+	install -d ${DESTDIR}${BINDIR} ${DESTDIR}${MANDIR}/man1
 	install operetta ${DESTDIR}${BINDIR}
+	install -m 644 doc/operetta.1 ${DESTDIR}${MANDIR}/man1
 clean:
-	rm precedent
-
+	rm operetta
 uninstall:
-	rm -f ${DESTDIR}${BINDIR}/operetta
+	-rm -f ${DESTDIR}${BINDIR}/operetta ${DESTDIR}${MANDIR}/man1/operetta.1
diff --git a/doc/operetta.1 b/doc/operetta.1
new file mode 100644
index 0000000..89a6de5
--- /dev/null
+++ b/doc/operetta.1
@@ -0,0 +1,92 @@
+.TH OPERETTA 1 "23 Feb 21" "Operetta version 0.1"
+.SH NAME
+operetta \- simple formal logic evaluator
+
+.SH SYNOPSIS
+\fBoperetta\fP <file> [--version] [--help] 
+
+.SH DESCRIPTION
+Operetta is a simple way to evaluate logical claims.
+Is it true that P implies P or Q? Operetta will tell you.
+
+.SH OPTIONS
+\fB--help\fP
+\-\- Displays usage info.
+
+\fB--version\fP
+\-\- Displays version info, and license information.
+
+.SH SYNTAX
+Operetta's syntax is fairly flexible. It is line based, so every proposition must be on its own line.
+It is whitespace dependent, so indents must be used only where applicable.
+Every line in operetta is split into two components--a proposition, and a justification.
+The proposition is essentially a statement. The base unit of a proposition is a variable,
+which is a letter or word that has a truth value. A variable is written as any letter or word in
+ALL CAPS. Suppose P stands for "it is raining".
+Writing [ P ] then means "it is raining." [ ~P ] means "it is not raining." The other component,
+the justification, is introduced by [ : ] or [ | ], following the proposition. A complete line looks
+like this: [ P | pr ], and is read "P is a premise." Most logical claims start with premises--things
+that are accepted to be true. From these premises, you may derive other truths. Suppose that you have
+[ P->Q | pr ], read as "P implies Q is a premise." If P implies Q, then whenever P is true, Q is too.
+Since P necessitates Q, you can derive Q from P. So, if the following two premises hold:
+[ P->Q | pr ], [ P | pr ], then [ Q | ->e x, x ] is true. Here, the justification is not a premise,
+it is the deductive rule called implication elimination. Implication elimination is a rule that
+justifies the right hand side of an proposition, if the proposition as a whole is true and the left hand side is true.
+Most rules follow a simple form: [ xe / xi ], where x is some connection in a proposition, i stands for introduction, and e stands for elimination.
+In this way, you can intuit the correct rule for a given application. Following the rule are two numbers,
+the lines that the justification references.
+
+.SH SYMBOLS
+\fB^\fP
+\-\- Conjunction, or AND.
+
+\fBv\fP
+\-\- Disjunction, or OR.
+
+\fB->\fP
+\-\- Implication.
+
+\fBu<->\fP
+\-\- Bi-implication.
+
+\fBu~ or !\fP
+\-\- Negation, or NOT.
+
+\fBu? or x\fP
+\-\- Contradiction.
+
+.SH RULES
+\fBpr\fP
+\-\- Premise. Always true, can only be defined in the top-most scope.
+
+\fBas\fP
+\-\- Assumption. Always true, but only in the new scope it creates.
+
+\fB^e\fP
+\-\- Conjunction elimination. Cite a proposition A^B. May justify either A or B.
+
+\fB^i\fP
+\-\- Conjunction introduction. Cite a proposition A and a proposition B. May justify A^B.
+
+\fBvi\fP
+\-\- Disjunction introduction. Cite a proposition A. May justify AvB, or BvA.
+
+\fB->e\fP
+\-\- Implication elimination. Cite a proposition A->B and a proposition A. May justify B.
+
+\fB->i\fP
+\-\- Implication introduction. Cite an assumption A, and a result of that assumption B. May justify A->B.
+
+\fBu?i or xi\fP
+\-\- Contradiction introduction. Cite a proposition A and a proposition ~A. May justify ? or x.
+
+\fBu~i or !i\fP
+\-\- Negation introduction. Cite an assumption A and a contradiction resulting from that assumption, B. May justify ~A.
+
+.SH AUTHOR
+Developed and maintained by Kai Stevenson.
+See git.aberrantflux.xyz/operetta.git for the latest version
+of the software.
+
+.SH "SEE ALSO"
+vi(1)