Kleene
Sections
ClassicalProps(jlc)
Doc
Def
3
== inr(inr(
))
is mentioned by
Thm*
x,y:
. x
y = 3
x = 3
y = 3
[K_or_equal_Three_2]
Thm*
x,y:
. x
y = 3
x = 3
& y = 3
[K_and_equal_Three_2]
Def
p
q == case p: 3
q; 3
case q: 3
3
; 3
3
; 3
3
;; 3
3
;
[K_or]
Def
p == case p: 3
3
; 3
3
; 3
3
;
[K_not]
Def
p
q == case p: 3
3
; 3
case q: 3
3
; 3
3
; 3
3
;; 3
q;
[K_imp]
In prior sections:
Three
Try larger context:
ClassicalProps(jlc)
Kleene
Sections
ClassicalProps(jlc)
Doc