refactoring ...

[helm.git] / helm / software / lambda-delta / examples / exp_math / L.hln

diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln
deleted file mode 100644 (file)
index 4b84f65..0000000
--- a/helm/software/lambda-delta/examples/exp_math/L.hln
+++ /dev/null
@@ -1,42 +0,0 @@
-\require preamble
-
-\* Intuitionistic Predicate Logic with Equality *\
-
-\open elements \* [1] 2.1. 2.2. 3.1 *\
-
-   \decl "logical false" False: *Prop
-
-   \decl "logical conjunction" And: *Prop => *Prop -> *Prop
-
-   \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
-
-\* implication and non-dependent abstraction are isomorphic *\
-   \def "logical implication" 
-      Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
-
-\* comprehension and dependent abstraction are isomorphic *\
-   \def "unrestricted logical comprehension"
-      All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
-
-   \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
-
-   \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
-
-\close
-
-\open abbreviations \* [1] 2.3. *\
-
-   \def "logical negation" 
-      Not = [p:*Prop] p -> False : *Prop -> *Prop
-
-   \def "logical equivalence"
-      Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
-
-   \def "unrestricted strict logical existence"
-      EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
-         : (*Obj -> *Prop) -> *Prop
-
-   \def "negated syntactical identity"
-      NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
-
-\close