#TODO
cc"""λ A :●. λ x :A. λ y :A. ●""" should typecheck...right?
val notNotLemTy = cc"""
Π A :●. (($not) (($not) (($lem) A)))""" //> notNotLemTy : cc.Cc.Exp = Π A : ● . ([λ B : ● . Π C : ● . C] ([λ
//| D : ● . Π E : ● . E] ([λ F : ● . ([λ G : ● . λ H : ● . Π I
//| : ● . Π J : [Π g : G . I] . Π K : [Π h : H . I] . I] F ([λ L : ● .
//| Π M : ● . M] F))] A)))
notNotLemTy.norm //> res16: cc.Cc.Exp = Π A : ● . Π B : ● . B
looks wrong...
parser: does parsing fully parens have performance issues?
The parser is known to non terminate on pathologically large terms
! CcParserSpec.can always parse a closed fully parened term: Exception rais
ed on property evaluation.
> ARG_0: λ _ : ● . ● → (Π A : ● . ● (● (● (● (□ (Π B : ● . (Π C : ● (((λ D
: ● . λ _ : (Π E : ● . ((λ _ : ● . ● (λ _ : (Π F : □ → ● → (λ _ : □ . ● (
(λ _ : □ → □ → □ (□ → (λ _ : ● . Π G : ● . Π H : (λ I : ● . (λ _ : (Π J :
● . (λ _ : ● (Π K : ● . ((λ L : ● . λ _ : ● ((● → ● → (λ _ : □ . (● (Π M
: ● . (Π N : □ . (Π O : (λ _ : (λ _ : (λ _ : ● (λ _ : □ . λ _ : ● . λ _
: (λ _ : (□ → (λ _ : □ . Π P : (● → (λ _ : □ . λ _ : ● . (λ _ : ● . λ _ :
□ . ((● (● ((λ _ : ● . ● → (λ _ : (Π Q : ● . (λ _ : (λ _ : ● . Π R : (λ
_ : □ . □ (λ _ : □ . λ _ : ● . λ _ : ● → (Π S : ● . Π T : (λ _ : □ (λ _ :
● . (λ _ : ● . ((λ _ : □ ((λ _ : (λ _ : (λ _ : □ (● (λ _ : (λ _ : (λ _ :
□ (λ _ : (λ _ : (Π U : (λ _ : □ . λ _ : (λ _ : ● . λ _ : (λ _ : □ (Π V :
● (● (λ _ : □ → (Π W : ● . λ _ : (λ _ : ● . Π X : □ . ((((Π Y : (λ _ : ●
. ● (● (□ (λ _ : ((λ _ : (Π Z : ● . λ _ : ● (● (□ (λ _ : □ ((λ _ : ● . (
□ → ● (● → (λ _ : ● . λ _ : ● . ● ((□ → (λ _ : □ . λ _ : ● → (λ _ : (λ _
: □ . Π A' : (Π B' : ● → ● (λ _ : ● . ● → (λ _ : ● . λ _ : (λ _ : (λ _ :
(Π C' : (Π D' : ● → □ → (λ _ : ● . (● → (Π E' : (Π F' : ● . □ (λ _ : (Π G
' : (Π H' : □ . (● → ● (● → (λ _ : □ . Π I' : ● (λ _ : (λ _ : (● → (λ _ :
(□ → (Π J' : (Π K' : ● . λ _ : ● (● (λ _ : (Π L' : ● . λ _ : (λ _ : (λ _
: ● . (λ _ : □ . Π M' : ● . λ _ : □ . (λ _ : ● . ● (λ _ : ● . λ _ : □ .
□ (λ _ : ● . ((((● → ● ((λ _ : ● . ● → ● → (λ _ : ● (□ → (λ _ : ((λ _ : ●
. λ _ : ● → ● → □ (□ → (λ _ : ● . ● → □)) ● . □) → ●) → ● . ●)) . ●)) →
●)) → □) → ●) → ●) → ●))) (λ _ : M' ● . ●)) ● L') . ●) . □) . ● (((K' → □
) → □) □ → □))) . ●) . □ → (λ _ : J' . ●))) → ● . □)) → ● . □) . ●) □ . I
' → ●) → ●)) → H') . ● → (λ _ : G' . ●) → □) . λ _ : F' . ●)) . (λ _ : ●
(λ _ : E' . ●) . ●) → ●)) □) → ● . λ _ : □ . D' → ●) ● . C') . ●) . ●) .
●)) . B') . A' ●) . □) . ●) → ●) → □)) ●)) ● ●) Z) . ●))) . □) . ●) ● → ●
) (X □) . □)))) . Y → □) → ●) → ●) → □) → □) . λ _ : (λ _ : W → ● . ●) .
●) . □)) ● → ● . ● (λ _ : ((λ _ : (λ _ : ● . V) . ●) → ●) → □ . ●) □) . ●
) → □ . □) . ●) . ● → (λ _ : U ● . □) □) . ●) . ●) . ●) . ●) □ . □)) . ●)
→ ● . ●) . □) → □) . □) → □) ●) ●) . S) . T) ● . □)) ● → ● . □ (● → ● (λ
_ : R . □))) . ●) Q) . □) → ●) ●)) → ●) → □) ●) ●)) → ● . ● ((λ _ : □ .
((λ _ : (λ _ : P □ ● . ●) . ●) → □) → □) □ → □)) □) → ● . □) . ●) . ●) .
●) → ● . □) . (λ _ : (λ _ : (λ _ : (□ → (λ _ : O . □)) → ● . ●) ● . ●) .
●) → ●) → N) (λ _ : M . ●) ● ● ●) → □) □ (λ _ : (λ _ : ● . Π M : ● . λ _
: □ → ● . M) . λ _ : ● . □))) ((Π M : L K ● . Π N : ● ● . λ _ : M . N) →
□)) . ●) → □) (K → ● ((λ _ : K . ●) ●) □ → (λ L : □ . (λ M : (λ N : ● . N
) (((λ _ : ● . ●) → ● → (λ _ : □ . □ (λ _ : (Π N : ● . N) . ●) → (● → ● →
●) □)) (□ → ●)) . M) → L ●))) . □) → J) □ (Π J : (λ _ : (λ _ : ((λ _ : ●
(λ _ : (λ K : □ . K) . □) . λ K : ● . λ k : K . k) ((λ g : G . g) → ●) →
(λ K : ● . K)) → (Π i : I . ((i → ●) → □) □) I . λ K : □ . λ L : ● . L K
) . I ●) . (λ K : ● (λ _ : (Π L : (Π M : □ → ● . λ _ : (λ m : M . (Π N :
□ . N) → (λ _ : (λ N : □ . Π O : (λ _ : □ . (λ _ : N . λ P : (Π Q : □ . Q
→ (λ R : (λ _ : Q . ●) □ ((((λ _ : ● . □) → (λ _ : □ → (λ _ : (λ S : ● .
λ _ : S (□ → S) (λ T : ● . λ _ : □ . T) □ . ●) → □ ● □ . ●) . ●)) → □ →
□) □) . ● (((λ _ : ● . □) → ● (λ S : (λ T : □ . λ _ : T □ . T) . (λ T : S
S . Π U : (λ V : (Π W : (λ s : S . ● s) (S (λ X : S → (λ _ : T . □) . X
□)) . λ _ : □ (W → □) . (λ _ : (λ X : ● . λ _ : X . ●) → ● . □) W) . ● V)
. λ V : □ . λ _ : U □ → (λ _ : ● . ●) . V) → ●)) → (λ _ : (λ _ : R . ●)
(λ _ : R . (λ S : (Π T : ● . T) . S ●) → □) . ●)) ● → R)) . P □) (λ P : (
Π Q : □ . Q) □ . □ (λ _ : (Π Q : ● . P ((□ → Q) (P ●))) . ●))) → □ . λ _
: N □ . O) m □ . □)) (□ (J → □ M) (λ _ : ((λ _ : (□ (□ J) → □) (□ ((Π N :
M (λ _ : □ . ●) . (● → (λ _ : N . λ O : ● . λ _ : □ → O . ● → (Π P : □ .
(Π Q : (λ _ : (λ _ : ● . P) . P) . (λ _ : □ . □) ((● P → □) Q)) ●))) (M
→ □)) → ●) (Π N : ● . ● N)) . ((Π N : ● . ● (Π O : (λ _ : □ . Π P : (λ Q
: □ . Π q : Q . (λ R : □ . Π S : (Π q1 : q . q1) . R ● → S → □ □) Q) . P)
(λ _ : □ (● ((λ _ : □ → (λ _ : ● . □) N → ● → (Π P : □ . ● (P → (λ _ : ●
. □)) P ((□ → ●) □)) . ●) (λ _ : □ . N) □)) N . λ _ : (λ P : □ . λ Q : (
λ _ : (Π R : (Π S : ● . λ T : (λ _ : (Π U : ● (P → □) (λ _ : (λ _ : □ S (
λ s : S . λ _ : s . λ _ : (Π V : □ . V) . □) . □) . λ _ : ● . □) . U) . ●
) . λ _ : □ . T) (λ S : (λ _ : P . ●) ((λ T : □ . (λ _ : T . □) → ●) (P (
(P → ●) → □) (□ → □))) → ● . (Π s : S . s) (Π T : S ● (□ (● S)) . S (T →
(λ t : T . t)) (● □))) . (λ _ : (λ r : R . r □ ●) . □) □) . □) . Q) . λ _
: ● . ●) (λ P : ● . ● ((□ → P) □)) . O)) M → □) ●) → □) ((λ _ : (λ N : ●
. λ O : N → □ . O (λ P : (Π Q : ● . Q) . (O → P) P)) → (λ _ : ● □ . ●) .
● ((λ _ : M . Π N : ● . λ O : (λ _ : □ . N) . N □ O □) □)) (● → (λ N : ●
. λ _ : (λ _ : ● . □ (Π O : (λ _ : □ . ●) □ . λ _ : O . (λ _ : (λ _ : ●
. ●) . □) ●)) ● → N . λ _ : □ . □) (λ _ : (λ _ : M . (● → ●) → □) . □)))
. □)) . ●) . L J ((λ _ : ● → (λ M : (Π N : ● → □ . N) . Π N : (λ _ : (λ _
: □ . M) . λ _ : ● (λ _ : ● . ●) . ●) . M → N) . L) → □ → ● (□ ●) → □))
. ●) . K ●) (J □ → J)) . (λ _ : ● . □) (λ _ : (λ _ : (Π J : I ((λ _ : □ .
□) □) . λ _ : J (λ K : ● ● . K) . J) . □) . ●)) → I) . λ _ : (λ I : □ .
H (Π J : (Π K : ● → (λ L : (λ i : I . i) . (λ M : (λ N : ● . Π O : (λ _ :
● ((λ _ : ((λ _ : L . □) → (λ P : (λ Q : (λ R : □ . (λ _ : ● (λ r : R .
r) (λ S : □ ● (λ T : (λ _ : R . □) → (λ _ : ● . (λ U : □ . U) □) . λ _ :
(λ U : T (T → ● → □ → □) . ● → (λ u : U . Π V : ● ● . λ W : u → (Π v : V
. v) . Π X : ● (□ (● (λ Y : (□ → ● (((λ Z : W → (λ _ : □ . ●) . Z → (λ A'
: (λ B' : □ . λ _ : □ . B' → □) . A')) → ●) (Π Z : ● . λ _ : Z Z . □)))
→ □ . W → (λ y : Y . □ → y (Π Z : □ . □ → Z)))) (λ Y : W □ . Y)) → □ . X
→ □)) . λ _ : ● . ● → (λ _ : (λ _ : ● → □ . λ _ : □ . ●) . □)) . (λ _ : S
. □ (□ □)) (λ _ : □ → □ . ● → ●)) . (Π S : □ . Π T : (λ _ : (λ _ : (Π U
: ● . U) . S) . ●) . (λ _ : (Π U : □ . Π V : (Π W : (Π X : ● . X) . □ → W
) . λ _ : (λ _ : (Π W : (Π X : (Π v : V . □ v □) . ((λ Y : □ . λ _ : (λ _
: (λ _ : (λ _ : ● . □) ((λ Z : ● □ → (λ _ : □ . □) . Z □ → (λ A' : □ . (
λ _ : (λ _ : (Π B' : □ . ● B') → □ . ●) (□ ● (λ _ : (λ _ : (Π a' : A' . λ
B' : (□ → a') (Π a'1 : A' . (λ _ : a'1 . a'1) → ●) . B') ● . A') . ●)) .
A') → □ (□ → ●) → □)) → □) . ●) . ● (λ _ : Y . ●)) . □) (V X → ●) → □ →
●) ● V) . λ _ : □ . λ _ : W . ● → (λ X : ● . X) → ●) . λ W : ● . λ _ : W
. W) (U → V) . □) (● → □) → □ . ●) → T) R) (λ S : (Π T : ● . (T (T → □) →
□) □) . (λ _ : (λ _ : (Π T : □ . T) . S S) . S) (λ T : □ R . (λ _ : ● .
●) (λ _ : T . T)) → S)) . Q) ● . P (P ● □ P ((λ _ : ● □ . □) → □) ●)) ●)
● (λ P : N □ → □ . P) → (λ _ : (λ P : □ → □ . (Π Q : □ . (λ R : □ (Π S :
(Π T : □ . (λ _ : (Q → ●) Q . □) T) . Q (λ _ : (λ _ : Q . □ (((λ T : □ .
T) → ●) ((Π T : □ . T) → □))) . S)) P → (λ S : ● . (● → S) ●) → ● . Π r :
R . λ _ : r . ●) ●) → ●) . □) . ●) → □) . □ N) → (Π P : (Π Q : (λ R : (Π
S : ● . S) . λ S : □ ((λ _ : R . ●) (λ T : (λ r : R . (□ → □ → □) r) . (
λ _ : ● T . □) (□ □))) . ● → S) . Q) . P → P) N . (λ n : N . (λ _ : n . ●
) → n) ((O → □) → O) (λ _ : ● . O)) ((L → ● ((Π N : (Π O : (λ _ : ● . □)
. λ _ : □ . O) . (λ _ : N . N) (λ O : □ . Π P : (N → O) → (● ● → ● → ●) →
□ . P → □)) → ●)) □) . M) ●) . λ _ : (λ _ : (λ _ : K . □) ● . □ → □) (λ
L : ● . ((K → □) → (λ _ : ● → □ . □) → □) L) . ●) . I ((λ _ : □ . ●) (● →
□ ● → ●)) (λ _ : (λ _ : ● (λ _ : ● ((● → ● ● □) J □ (□ → (λ _ : □ . ●)))
□ . □) . J) → J (J ((Π j : J . j □) → ●)) . ●))) . H)) . □) ●)) . F) . ●
) □ → ● ●) → (Π e : E . e □ (λ e1 : e . ● (e1 □)) → □) □) D) (λ E : ● . λ
F : E → ● E . Π G : (Π H : □ . (λ I : (λ _ : ● . ●) . Π J : ● . ((λ K :
● (● (□ (□ → (Π L : ● . λ _ : ● . L)) I)) . ● (λ L : (λ _ : (λ _ : K . □)
. ●) . (λ _ : (Π M : (Π N : (Π O : (Π P : (λ Q : ● . Π q : Q . q) . P (λ
Q : (Π R : □ . (λ S : ● → R . R (λ T : (λ U : ● . U □) . (Π U : (λ _ : S
(● (λ _ : S . ● ●)) (□ → (λ _ : T . □)) . ●) . ● (λ V : (λ _ : (λ W : T
□ . ((W ● → (λ _ : W . ●)) ● → (λ _ : ● W . □)) → (Π X : (λ Y : □ . Y) .
X → ●)) . U) . Π W : □ (● □ ●) □ . Π X : ● (□ (λ Y : (λ _ : □ . □) (λ _ :
V . W ●) (λ _ : ● . ● (● → □)) . □ □ → Y)) . λ _ : ● . (X → ●) → □)) ((●
→ □) (λ U : □ . λ _ : (λ _ : (λ _ : ● → ● (□ ((λ V : ● → □ . λ _ : V . V
) ●)) □ . □) . λ _ : □ . λ _ : □ . λ V : ● ● . λ W : (Π X : ● . X) → ● .
λ X : ((● → (λ _ : (Π Y : W → (Π Z : (λ _ : □ → (λ _ : (λ A' : □ . A' (λ
_ : ● . A')) . □) . □ □) . λ _ : (Π A' : ● (Π B' : Z → ● . (B' (λ _ : Z .
□ → □) → ●) → (Π C' : ● → ● . □ → C')) . λ _ : (● → A') (□ (A' (□ Z))) .
A') Z . ● → (λ _ : ● . ●)) . λ _ : (λ _ : □ . ●) ● Y . ●) . □)) → W) V .
λ Y : (λ Z : □ ● . (● → ●) (● (λ _ : (λ _ : Z . Z) (● → (Π A' : Z → □ □
. A')) . ●))) . Π Z : (λ _ : (λ A' : (Π x : X . x (λ _ : x . □)) . (λ _ :
(Π B' : □ . B') . □) (A' Y) □) . ●) . ● ((λ A' : (λ _ : □ . □) . λ _ : (
λ _ : □ . A') . □) (□ ●)) (● (λ _ : □ . □)) → (λ _ : □ Z . □) → ● □) . U)
))) → ●) (λ R : ● ● . λ _ : P . R) . (λ _ : Q (λ _ : (λ _ : Q (((Π R : (Π
q : Q . q) . ● (Q → R)) → ● → (λ _ : ● → (λ _ : (Π R : ● . R) . □ → ●) .
□)) (□ ((λ R : (Π p : P . p) → Q . λ _ : R . ●) (λ R : (λ S : P → □ (λ _
: □ . □) . λ _ : S . ●) . ● □ R (R → R) → R) Q))) (● ●) □ (Q → Q) → (λ _
: (Π R : ● . R) . ●) . λ _ : (□ → ●) → (λ R : □ . R) . ●) . ●) . ● → ●)
(λ R : ● . λ S : (λ _ : (Π T : (Π r : R . □ → r) . T) . R) . Π T : (λ _ :
(λ _ : S (● (□ R)) . □ ● ((□ → ●) ●)) . ●) . T) → (Π R : □ . □ R → R)))
. λ _ : □ . O) → □ . (λ O : ● L . □ ((λ _ : (λ _ : ● . O) . ●) → (λ _ : □
. □))) (□ ((λ _ : □ . ● → ●) N))) . M □) . □) □) → ● (λ L : ● . L)) → □)
(□ → J) (□ → J)) (● (□ ●) (λ _ : F . H))) F . G) . D) ((λ _ : (λ _ : □ .
λ D : ● . D (λ _ : ((λ _ : □ → ● . Π E : □ . E) → ●) → ● → □ . λ _ : □ .
●)) (B □ → □) . λ D : □ . D) → (λ _ : □ → ● □ . ●)) → ●) □ → ● □) → ● .
λ _ : (λ D : ● . □ → (Π d : D . d)) . C) → (● → ●) (Π C : ● . □ (λ D : ●
. D) ((λ _ : ((λ _ : □ . λ _ : (λ D : (λ _ : ● . ●) ● . D) . ●) ● → (λ D
: ● . Π d : D . ((λ _ : d ● . Π d1 : d . λ _ : (λ _ : ● . □) . d1) → □) □
)) → C . □) (λ _ : □ . ●))))) → □)) (λ _ : (Π a : A . λ B : □ a . B) → ●
. □ □)))