aboutsummaryrefslogtreecommitdiffhomepage
path: root/twelf/example.elf
diff options
context:
space:
mode:
Diffstat (limited to 'twelf/example.elf')
-rw-r--r--twelf/example.elf5
1 files changed, 5 insertions, 0 deletions
diff --git a/twelf/example.elf b/twelf/example.elf
index e52d5a06..b4281734 100644
--- a/twelf/example.elf
+++ b/twelf/example.elf
@@ -4,6 +4,11 @@
%%% $Id$
%%%
+%%% Rather than a proof this file is just a signature,
+%%% bunch of declarations. Would be nice to have something
+%%% closer to other systems for pedagogical purposes...
+%%% (i.e. proving commutativity of conjunction in ND fragment
+%%% of this logic)
%%% Intuitionistic propositional calculus
%%% Positive fragment with implies, and, true.