mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-05 19:27:30 +03:00
Fix some syntaxes uses of switch +: to _:
This commit is contained in:
parent
3ce20b7003
commit
144c3210df
@ -10,7 +10,7 @@ BBT.has.linear
|
||||
use bin = λsize λnode_key λval λlft λrgt
|
||||
use P = λx
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(size: #U60)
|
||||
∀(size: U60)
|
||||
∀(node_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
|
@ -140,7 +140,7 @@ Kind.Term.show.go
|
||||
z
|
||||
dep
|
||||
(Kind.Text.show.go
|
||||
"; +: "
|
||||
"; _: "
|
||||
(Kind.Term.show.go
|
||||
(s (Kind.var (String.concat nam "-1") dep))
|
||||
(Nat.succ dep)
|
||||
|
@ -12,7 +12,7 @@ Kind.reduce.mat
|
||||
use Y = λx.val
|
||||
switch x = x.val {
|
||||
0: λz λs (Kind.reduce maj z)
|
||||
+: λz λs (Kind.reduce maj (s (Kind.num x-1)))
|
||||
_: λz λs (Kind.reduce maj (s (Kind.num x-1)))
|
||||
}: ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term)
|
||||
Kind.Term
|
||||
use N = λx λz λs (Kind.mat nam x z s p)
|
||||
|
@ -8,9 +8,9 @@ QBool
|
||||
∀(x:
|
||||
switch t = t {
|
||||
0: (P QBool.true)
|
||||
+: switch t = t-1 {
|
||||
_: switch t = t-1 {
|
||||
0: (P QBool.false)
|
||||
+: ∀(x: Empty) *
|
||||
_: ∀(x: Empty) *
|
||||
}: *
|
||||
}: *
|
||||
)
|
||||
|
@ -10,15 +10,15 @@ QBool.match
|
||||
λtag
|
||||
switch tag = tag {
|
||||
0: λx (x t)
|
||||
+: λx
|
||||
_: λx
|
||||
(switch tag_1 = tag-1 {
|
||||
0: λx (x f)
|
||||
+: λx (x λe (Empty.absurd e *))
|
||||
_: λx (x λe (Empty.absurd e *))
|
||||
}: ∀(x:
|
||||
∀(x:
|
||||
switch tag_1 = tag_1 {
|
||||
0: (P QBool.false)
|
||||
+: ∀(x: Empty) *
|
||||
_: ∀(x: Empty) *
|
||||
}: *
|
||||
)
|
||||
(P a)
|
||||
@ -30,9 +30,9 @@ QBool.match
|
||||
∀(x:
|
||||
switch tag = tag {
|
||||
0: (P QBool.true)
|
||||
+: switch tag_1 = tag-1 {
|
||||
_: switch tag_1 = tag-1 {
|
||||
0: (P QBool.false)
|
||||
+: ∀(x: Empty) *
|
||||
_: ∀(x: Empty) *
|
||||
}: *
|
||||
}: *
|
||||
)
|
||||
|
@ -6,9 +6,9 @@ QBool2
|
||||
∀(tag: U60)
|
||||
switch tag = tag {
|
||||
0: (P QBool2.true)
|
||||
+: switch tag_1 = tag-1 {
|
||||
_: switch tag_1 = tag-1 {
|
||||
0: (P QBool2.false)
|
||||
+: ∀(e: Empty) *
|
||||
_: ∀(e: Empty) *
|
||||
}: *
|
||||
}: *
|
||||
)
|
||||
|
@ -10,18 +10,18 @@ QBool2.match
|
||||
λtag
|
||||
switch tag = tag {
|
||||
0: t
|
||||
+: switch tag_1 = tag-1 {
|
||||
_: switch tag_1 = tag-1 {
|
||||
0: f
|
||||
+: λe (~e λx *)
|
||||
_: λe (~e λx *)
|
||||
}: switch tag_1 = tag_1 {
|
||||
0: (P QBool2.false)
|
||||
+: ∀(e: Empty) *
|
||||
_: ∀(e: Empty) *
|
||||
}: *
|
||||
}: switch tag = tag {
|
||||
0: (P QBool2.true)
|
||||
+: switch tag_1 = tag-1 {
|
||||
_: switch tag_1 = tag-1 {
|
||||
0: (P QBool2.false)
|
||||
+: ∀(e: Empty) *
|
||||
_: ∀(e: Empty) *
|
||||
}: *
|
||||
}: *
|
||||
)
|
||||
|
@ -7,6 +7,6 @@ QUnit
|
||||
λtag
|
||||
switch tag = tag {
|
||||
0: ∀(one: (P QUnit.one)) (P self)
|
||||
+: Empty
|
||||
_: Empty
|
||||
}: *
|
||||
)
|
@ -3,5 +3,5 @@ U60.equal
|
||||
= λa λb
|
||||
switch x = (== a b) {
|
||||
0: Bool.false
|
||||
+: Bool.true
|
||||
_: Bool.true
|
||||
}: Bool
|
||||
|
@ -1,3 +1,3 @@
|
||||
U60.if
|
||||
: ∀(x: U60) ∀(P: *) ∀(t: P) ∀(f: P) P
|
||||
= λx λP λt λf switch x = x { 0: t +: f }: P
|
||||
= λx λP λt λf switch x = x { 0: t _: f }: P
|
@ -5,4 +5,4 @@ U60.switch
|
||||
∀(z: (P 0))
|
||||
(P x)
|
||||
= λx λP λs λz
|
||||
switch self = x { 0: z +: (s self-1) }: (P self)
|
||||
switch self = x { 0: z _: (s self-1) }: (P self)
|
@ -3,7 +3,7 @@ U60.name.go
|
||||
= λn
|
||||
switch n = n {
|
||||
0: λnil nil
|
||||
+: λnil
|
||||
_: λnil
|
||||
(String.cons
|
||||
(+ 97 (% n-1 26))
|
||||
(U60.name.go (/ n-1 26) nil)
|
||||
|
@ -7,5 +7,5 @@ U60.show.go
|
||||
(/ n 10)
|
||||
(String.cons (+ 48 (% n 10)) nil)
|
||||
)
|
||||
+: λnil (String.cons (+ 48 n) nil)
|
||||
_: λnil (String.cons (+ 48 n) nil)
|
||||
}: String.Concatenator
|
@ -1,5 +1,5 @@
|
||||
U60.to_bool (x: U60) : Bool =
|
||||
switch x {
|
||||
0: Bool.false
|
||||
+: Bool.true
|
||||
_: Bool.true
|
||||
}: Bool
|
||||
|
Loading…
Reference in New Issue
Block a user