mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
28 lines
779 B
Text
28 lines
779 B
Text
type0 : Type
|
|
typeof(type0) : Type.{2}
|
|
type tower: [Type;Type.{2};Type.{3};Type.{4};Type.{5}]
|
|
Bool: [true, false]
|
|
a: a, b: b, typeof(a): Bool
|
|
b2b: (Bool -> Bool)
|
|
p(a): (p a)
|
|
p(b): (p b)
|
|
q(a): (q a)
|
|
q(b): (q b)
|
|
typeof(p a): Bool
|
|
lxy_px: (\x:Bool. (\y:Bool. (p x[1])))
|
|
type: (Bool -> (Bool -> Bool))
|
|
type of type: Type
|
|
lxy_px a b: ((\x:Bool. (\y:Bool. (p x[1]))) a b)
|
|
type: Bool
|
|
(=): =
|
|
type: (Pi A:Type. (Pi _:A[0]. (A[1] -> Bool)))
|
|
p2: p2
|
|
type: (tau -> (tau -> Bool))
|
|
t2: (= (tau -> (tau -> Bool)) (\x:tau. (\y:tau. (p2 x[1] y[0]))) (= tau))
|
|
type: Bool
|
|
f_vec: vec
|
|
type: (Type -> (nat -> Type))
|
|
type of type: Type.{2}
|
|
f_vec_weird: vec?
|
|
type: (Pi A:Type.{l1}. (Pi n:Type.{l2 + 1}. Type.{max(l1, l2)}))
|
|
type of type: Type.{imax(l1, imax(l2 + 1, max(l1, l2))) + 1}
|