diff --git a/book/BMap/leaf.kind2 b/book/BMap/leaf.kind2 index 114936a6..2a6e6418 100644 --- a/book/BMap/leaf.kind2 +++ b/book/BMap/leaf.kind2 @@ -1,3 +1,4 @@ BMap/leaf : ∀(A: *) (BMap A) -= λA ~λP λnode λleaf leaf + +λA ~λP λnode λleaf leaf diff --git a/book/BMap/node.kind2 b/book/BMap/node.kind2 index 9c835809..25daec06 100644 --- a/book/BMap/node.kind2 +++ b/book/BMap/node.kind2 @@ -4,5 +4,6 @@ BMap/node ∀(val: A) ∀(rgt: (BMap A)) (BMap A) -= λA λlft λval λrgt - ~λP λnode λleaf (node lft val rgt) + +λA λlft λval λrgt +~λP λnode λleaf (node lft val rgt) diff --git a/book/Bool/and.kind2 b/book/Bool/and.kind2 index 1eb7f560..358a591d 100644 --- a/book/Bool/and.kind2 +++ b/book/Bool/and.kind2 @@ -1,7 +1,11 @@ use Bool/{true,false,and} -and (a: Bool) (b: Bool) : Bool = - match a { - true: b - false: false - } +and +- a: Bool +- b: Bool +: Bool + +match a { + true: b + false: false +} diff --git a/book/Bool/false.kind2 b/book/Bool/false.kind2 index 5a736688..4fa76fb3 100644 --- a/book/Bool/false.kind2 +++ b/book/Bool/false.kind2 @@ -1,2 +1,4 @@ -false : Bool = - ~λP λt λf f +false +: Bool + +~λP λt λf f diff --git a/book/Bool/if.kind2 b/book/Bool/if.kind2 index 3a70fcd5..87f45c84 100644 --- a/book/Bool/if.kind2 +++ b/book/Bool/if.kind2 @@ -1,7 +1,13 @@ use Bool/{true,false} -if (b: Bool) (P: *) (t: P) (f: P) : P = - match b { - true: t - false: f - } +if +- b: Bool +- P: * +- t: P +- f: P +: P + +match b { + true: t + false: f +} diff --git a/book/Bool/match.kind2 b/book/Bool/match.kind2 index 181a72dd..a7524f7d 100644 --- a/book/Bool/match.kind2 +++ b/book/Bool/match.kind2 @@ -1,9 +1,10 @@ use Bool/{true,false} match - (P: ∀(x: Bool) *) - (t: (P true)) - (f: (P false)) - (b: Bool) +- P: ∀(x: Bool) * +- t: (P true) +- f: (P false) +- b: Bool : (P b) -= (~b P t f) + +(~b P t f) diff --git a/book/Bool/not.kind2 b/book/Bool/not.kind2 index 39bdd0dd..e6edca78 100644 --- a/book/Bool/not.kind2 +++ b/book/Bool/not.kind2 @@ -1,7 +1,10 @@ use Bool/{true,false} -not (x: Bool) : Bool = - match x { - true: false - false: true - } +not +- x: Bool +: Bool + +match x { + true: false + false: true +} diff --git a/book/Bool/or.kind2 b/book/Bool/or.kind2 index c847f174..302f7891 100644 --- a/book/Bool/or.kind2 +++ b/book/Bool/or.kind2 @@ -1,7 +1,11 @@ use Bool/{true,false} -or (a: Bool) (b: Bool) : Bool = - match a { - true: true - false: b - } +or +- a: Bool +- b: Bool +: Bool + +match a { + true: true + false: b +} diff --git a/book/Bool/show.kind2 b/book/Bool/show.kind2 index 7b8ae027..33b497f4 100644 --- a/book/Bool/show.kind2 +++ b/book/Bool/show.kind2 @@ -1,7 +1,10 @@ use Bool/{true,false} -show (x: Bool) : String = - match x { - true: "true" - false: "false" - } +show +- x: Bool +: String + +match x { + true: "true" + false: "false" +} diff --git a/book/Bool/true.kind2 b/book/Bool/true.kind2 index dcc3aaa1..959ca757 100644 --- a/book/Bool/true.kind2 +++ b/book/Bool/true.kind2 @@ -1,2 +1,4 @@ -true : Bool = - ~λP λt λf t +true +: Bool + +~λP λt λf t diff --git a/book/Char/equal.kind2 b/book/Char/equal.kind2 index 2368c866..35e76c8b 100644 --- a/book/Char/equal.kind2 +++ b/book/Char/equal.kind2 @@ -1,2 +1,6 @@ -equal (a: Char) (b: Char) : Bool = - (U48/equal a b) +equal +- a: Char +- b: Char +: Bool + +(U48/equal a b) diff --git a/book/Char/is_between.kind2 b/book/Char/is_between.kind2 index 630b9ac6..6e49ec60 100644 --- a/book/Char/is_between.kind2 +++ b/book/Char/is_between.kind2 @@ -1,4 +1,9 @@ -is_between (min: Char) (max: Char) (chr: Char) : Bool = - (Bool/and - (U48/to_bool (>= chr min)) - (U48/to_bool (<= chr max))) +is_between +- min: Char +- max: Char +- chr: Char +: Bool + +(Bool/and + (U48/to_bool (>= chr min)) + (U48/to_bool (<= chr max))) diff --git a/book/Char/is_blank.kind2 b/book/Char/is_blank.kind2 index a894ab26..870266db 100644 --- a/book/Char/is_blank.kind2 +++ b/book/Char/is_blank.kind2 @@ -1,2 +1,5 @@ -is_blank (a: Char) : Bool = - (Bool/or (Char/equal a 10) (Char/equal a 32)) +is_blank +- a: Char +: Bool + +(Bool/or (Char/equal a 10) (Char/equal a 32)) diff --git a/book/Char/is_decimal.kind2 b/book/Char/is_decimal.kind2 index df24aaad..60790c84 100644 --- a/book/Char/is_decimal.kind2 +++ b/book/Char/is_decimal.kind2 @@ -1,2 +1,5 @@ -is_decimal (a: Char) : Bool = - (Char/is_between 48 57 a) +is_decimal +- a: Char +: Bool + +(Char/is_between 48 57 a) diff --git a/book/Char/is_name.kind2 b/book/Char/is_name.kind2 index 46e5cdb3..60b852bb 100644 --- a/book/Char/is_name.kind2 +++ b/book/Char/is_name.kind2 @@ -1,13 +1,14 @@ use Bool/{true,false,or} use Char/{is_between,equal} -is_name (a: Char) : Bool = - (or (is_between 97 122 a) - (or (is_between 65 90 a) - (or (is_between 48 57 a) - (or (equal 95 a) - (or (equal 46 a) - (or (equal 45 a) - false)))))) - +is_name +- a: Char +: Bool +(or (is_between 97 122 a) +(or (is_between 65 90 a) +(or (is_between 48 57 a) +(or (equal 95 a) +(or (equal 46 a) +(or (equal 45 a) +false)))))) diff --git a/book/Char/is_newline.kind2 b/book/Char/is_newline.kind2 index 21532c8a..8575a97f 100644 --- a/book/Char/is_newline.kind2 +++ b/book/Char/is_newline.kind2 @@ -1,2 +1,5 @@ -is_newline (a: Char) : Bool = - (Char/equal a 10) +is_newline +- a: Char +: Bool + +(Char/equal a 10) diff --git a/book/Char/is_oper.kind2 b/book/Char/is_oper.kind2 index 649cd5a5..eb51ef6b 100644 --- a/book/Char/is_oper.kind2 +++ b/book/Char/is_oper.kind2 @@ -1,18 +1,21 @@ use Bool/{true,false,or} use Char/{equal} -is_oper (a: Char) : Bool = - (or (equal 43 a) - (or (equal 45 a) - (or (equal 42 a) - (or (equal 47 a) - (or (equal 37 a) - (or (equal 60 a) - (or (equal 62 a) - (or (equal 61 a) - (or (equal 38 a) - (or (equal 124 a) - (or (equal 94 a) - (or (equal 33 a) - (or (equal 126 a) - false))))))))))))) +is_oper +- a: Char +: Bool + +(or (equal 43 a) +(or (equal 45 a) +(or (equal 42 a) +(or (equal 47 a) +(or (equal 37 a) +(or (equal 60 a) +(or (equal 62 a) +(or (equal 61 a) +(or (equal 38 a) +(or (equal 124 a) +(or (equal 94 a) +(or (equal 33 a) +(or (equal 126 a) +false))))))))))))) diff --git a/book/Char/is_slash.kind2 b/book/Char/is_slash.kind2 index ac7d7723..f8191d70 100644 --- a/book/Char/is_slash.kind2 +++ b/book/Char/is_slash.kind2 @@ -1,2 +1,5 @@ -is_slash (a: Char) : Bool = - (Char/equal a 47) +is_slash +- a: Char +: Bool + +(Char/equal a 47) diff --git a/book/Cmp/eql.kind2 b/book/Cmp/eql.kind2 index fa6436a7..5c9ac313 100644 --- a/book/Cmp/eql.kind2 +++ b/book/Cmp/eql.kind2 @@ -1,2 +1,3 @@ -eql : Cmp = - ~λP λltn λeql λgtn eql +eql : Cmp + +~λP λltn λeql λgtn eql diff --git a/book/Cmp/gtn.kind2 b/book/Cmp/gtn.kind2 index 3d13adeb..db7f8c41 100644 --- a/book/Cmp/gtn.kind2 +++ b/book/Cmp/gtn.kind2 @@ -1,2 +1,3 @@ -Cmp/gtn : Cmp = - ~λP λltn λeql λgtn gtn +Cmp/gtn : Cmp + +~λP λltn λeql λgtn gtn diff --git a/book/Cmp/is_gtn.kind2 b/book/Cmp/is_gtn.kind2 index d0feec7c..e166afbe 100644 --- a/book/Cmp/is_gtn.kind2 +++ b/book/Cmp/is_gtn.kind2 @@ -1,9 +1,12 @@ use Bool/{true,false} use Cmp/{ltn,eql,gtn} -Cmp/is_gtn (cmp: Cmp) : Bool - = match cmp { - ltn: false - eql: false - gtn: true - } +Cmp/is_gtn +- cmp: Cmp +: Bool + +match cmp { + ltn: false + eql: false + gtn: true +} diff --git a/book/Cmp/ltn.kind2 b/book/Cmp/ltn.kind2 index a0a4cb6a..007c9d58 100644 --- a/book/Cmp/ltn.kind2 +++ b/book/Cmp/ltn.kind2 @@ -1,2 +1,3 @@ -Cmp/ltn : Cmp = - ~λP λltn λeql λgtn ltn +Cmp/ltn : Cmp + +~λP λltn λeql λgtn ltn diff --git a/book/Cmp/match.kind2 b/book/Cmp/match.kind2 index 7ee08d43..efe0418b 100644 --- a/book/Cmp/match.kind2 +++ b/book/Cmp/match.kind2 @@ -1,8 +1,9 @@ Cmp/match - (P: Cmp -> *) - (l: (P Cmp/ltn)) - (e: (P Cmp/eql)) - (g: (P Cmp/gtn)) - (c: Cmp) -: (P c) = - (~c P l e g) +- P: Cmp -> * +- l: (P Cmp/ltn) +- e: (P Cmp/eql) +- g: (P Cmp/gtn) +- c: Cmp +: (P c) + +(~c P l e g) diff --git a/book/Empty/absurd.kind2 b/book/Empty/absurd.kind2 index ed478a9d..911a2a4a 100644 --- a/book/Empty/absurd.kind2 +++ b/book/Empty/absurd.kind2 @@ -1,2 +1,6 @@ -absurd (e: Empty) (P: *) : P = - (~e λx(P)) +absurd +- e: Empty +- P: * +: P + +(~e λx(P)) diff --git a/book/Equal/apply.kind2 b/book/Equal/apply.kind2 index 346124e8..5a9aea57 100644 --- a/book/Equal/apply.kind2 +++ b/book/Equal/apply.kind2 @@ -1,4 +1,8 @@ -apply (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) = - match e { - Equal/refl: ~λPλe(e (f e.a)) - }: (Equal B (f a) (f b)) +apply +- f: A -> B +- e: (Equal A a b) +: (Equal B (f a) (f b)) + +match e { + Equal/refl: ~λPλe(e (f e.a)) +}: (Equal B (f a) (f b)) diff --git a/book/Equal/match.kind2 b/book/Equal/match.kind2 index 0ab1f1fb..9e6535c8 100644 --- a/book/Equal/match.kind2 +++ b/book/Equal/match.kind2 @@ -1,6 +1,7 @@ match - (P: ∀(a:T) ∀(b:T) ∀(e: (Equal T a b)) *) - (refl: ∀(x: T) (P x x (Equal/refl T x))) - (e: (Equal T a b)) -: (P a b e) = - (~e P refl) +- P: ∀(a:T) ∀(b:T) ∀(e: (Equal T a b)) * +- refl: ∀(x: T) (P x x (Equal/refl T x)) +- e: (Equal T a b) +: (P a b e) + +(~e P refl) diff --git a/book/Equal/refl.kind2 b/book/Equal/refl.kind2 index 59b11233..8823257f 100644 --- a/book/Equal/refl.kind2 +++ b/book/Equal/refl.kind2 @@ -1,2 +1,5 @@ -refl (x: A) : (Equal A x x) = - ~ λP λrefl (refl x) +refl +- x: A +: (Equal A x x) + +~ λP λrefl (refl x) diff --git a/book/IO/bind.kind2 b/book/IO/bind.kind2 index f3e75248..ce79adef 100644 --- a/book/IO/bind.kind2 +++ b/book/IO/bind.kind2 @@ -1,29 +1,11 @@ -bind (a: (IO A)) (b: A -> (IO B)) : (IO B) = - match a { - IO/print: (IO/print B a.text λx (IO/bind A B (a.then x) b)) - IO/load: (IO/load B a.file λs (IO/bind A B (a.then s) b)) - IO/save: (IO/save B a.file a.text λx (IO/bind A B (a.then Unit/new) b)) - IO/done: (b a.term) - } +bind +- a: (IO A) +- b: A -> (IO B) +: (IO B) -//IO/bind -//: ∀(A: *) - //∀(B: *) - //∀(a: (IO A)) - //∀(b: ∀(x: A) (IO B)) - //(IO B) -//= λA λB λa λb - //use P = λx ∀(b: ∀(x: A) (IO B)) (IO B) - //use print = λtext λthen λb - //(IO/print B text λx (IO/bind A B (then x) b)) - //use load = λfile λthen λb - //(IO/load B file λs (IO/bind A B (then s) b)) - //use save = λfile λdata λthen λb - //(IO/save - //B - //file - //data - //λx (IO/bind A B (then Unit/one) b) - //) - //use done = λterm λb (b term) - //(~a P print load save done b) +match a { + IO/print: (IO/print B a.text λx (IO/bind A B (a.then x) b)) + IO/load: (IO/load B a.file λs (IO/bind A B (a.then s) b)) + IO/save: (IO/save B a.file a.text λx (IO/bind A B (a.then Unit/new) b)) + IO/done: (b a.term) +} diff --git a/book/IO/done.kind2 b/book/IO/done.kind2 index 2f874fe3..b4c5cd3a 100644 --- a/book/IO/done.kind2 +++ b/book/IO/done.kind2 @@ -1,3 +1,4 @@ IO/done : ∀(A: *) ∀(term: A) (IO A) -= λA λterm ~λP λprint λload λsave λdone (done term) + +λA λterm ~λP λprint λload λsave λdone (done term) diff --git a/book/IO/load.kind2 b/book/IO/load.kind2 index 62840748..d1aea1c4 100644 --- a/book/IO/load.kind2 +++ b/book/IO/load.kind2 @@ -3,5 +3,6 @@ IO/load ∀(file: String) ∀(then: ∀(x: String) (IO A)) (IO A) -= λA λfile λthen - ~λP λprint λload λsave λdone (load file then) + +λA λfile λthen +~λP λprint λload λsave λdone (load file then) diff --git a/book/IO/match.kind2 b/book/IO/match.kind2 index b75a458a..2527b397 100644 --- a/book/IO/match.kind2 +++ b/book/IO/match.kind2 @@ -1,9 +1,10 @@ match - (P: (IO A) -> *) - (print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/print A text then))) - (load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO/load A file then))) - (save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/save A file text then))) - (done: ∀(term: A) (P (IO/done A term))) - (x: (IO A)) -: (P x) = - (~x P print load save done) +- P: (IO A) -> * +- print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/print A text then)) +- load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO/load A file then)) +- save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/save A file text then)) +- done: ∀(term: A) (P (IO/done A term)) +- x: (IO A) +: (P x) + +(~x P print load save done) diff --git a/book/IO/print.kind2 b/book/IO/print.kind2 index 316ef7a1..3c044a3c 100644 --- a/book/IO/print.kind2 +++ b/book/IO/print.kind2 @@ -1,5 +1,6 @@ IO/print : ∀(A: *) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (IO A) -= λA λtext λthen - ~λP λprint λload λsave λdone (print text then) + +λA λtext λthen +~λP λprint λload λsave λdone (print text then) diff --git a/book/IO/run.kind2 b/book/IO/run.kind2 index f01416a2..a1f50432 100644 --- a/book/IO/run.kind2 +++ b/book/IO/run.kind2 @@ -1,20 +1,10 @@ -run (x: (IO A)) : (IO A) = - match x { - IO/print: (IO/print A x.text λu (run A (x.then Unit/new))) - IO/load: (IO/load A x.file λs (run A (x.then s))) - IO/save: (IO/save A x.file x.text λu (run A (x.then Unit/new))) - IO/done: (IO/done A x.term) - } +run +- x: (IO A) +: (IO A) -//IO/run -//: ∀(A: *) ∀(x: (IO A)) (IO A) -//= λA λx - //use P = λx (IO A) - //use print = λtext λthen - //(IO/print A text λu (IO/run A (then Unit/new))) - //use load = λfile λthen - //(IO/load A file λs (IO/run A (then s))) - //use save = λfile λtext λthen - //(IO/save A file text λu (IO/run A (then Unit/new))) - //use done = λterm (IO/done A term) - //(~x P print load save done) +match x { + IO/print: (IO/print A x.text λu (run A (x.then Unit/new))) + IO/load: (IO/load A x.file λs (run A (x.then s))) + IO/save: (IO/save A x.file x.text λu (run A (x.then Unit/new))) + IO/done: (IO/done A x.term) +} diff --git a/book/IO/save.kind2 b/book/IO/save.kind2 index c589005a..c4244dea 100644 --- a/book/IO/save.kind2 +++ b/book/IO/save.kind2 @@ -4,5 +4,6 @@ IO/save ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (IO A) -= λA λfile λtext λthen - ~λP λprint λload λsave λdone (save file text then) + +λA λfile λtext λthen +~λP λprint λload λsave λdone (save file text then) diff --git a/book/List/and.kind2 b/book/List/and.kind2 index abe1b8dd..204ad489 100644 --- a/book/List/and.kind2 +++ b/book/List/and.kind2 @@ -1,8 +1,11 @@ use List/{cons,nil} use Bool/{true} -and (list: (List Bool)) : Bool = - fold list { - cons: (Bool/and list.head list.tail) - nil: true - } +and +- list: (List Bool) +: Bool + +fold list { + cons: (Bool/and list.head list.tail) + nil: true +} diff --git a/book/List/begin.kind2 b/book/List/begin.kind2 index cdd357c2..bf95d49c 100644 --- a/book/List/begin.kind2 +++ b/book/List/begin.kind2 @@ -1,10 +1,13 @@ use List/{cons,nil} -begin (xs: (List A)) : (List A) = - match xs { - cons: match xs.tail { - cons: (cons _ xs.head (begin _ (cons _ xs.tail.head xs.tail.tail))) - nil: (cons _ xs.head (nil _)) - } - nil: (nil _) +begin +- xs: (List A) +: (List A) + +match xs { + cons: match xs.tail { + cons: (cons _ xs.head (begin _ (cons _ xs.tail.head xs.tail.tail))) + nil: (cons _ xs.head (nil _)) } + nil: (nil _) +} diff --git a/book/List/concat.kind2 b/book/List/concat.kind2 index 4084db03..fd6fcc4c 100644 --- a/book/List/concat.kind2 +++ b/book/List/concat.kind2 @@ -1,7 +1,11 @@ use List/{cons,nil} -concat (xs: (List T)) (ys: (List T)) : (List T) = - match xs { - cons: (cons _ xs.head (concat _ xs.tail ys)) - nil: ys - } +concat +- xs: (List T) +- ys: (List T) +: (List T) + +match xs { + cons: (cons _ xs.head (concat _ xs.tail ys)) + nil: ys +} diff --git a/book/List/cons.kind2 b/book/List/cons.kind2 index b1a84b3f..a43ea709 100644 --- a/book/List/cons.kind2 +++ b/book/List/cons.kind2 @@ -1,2 +1,6 @@ -cons (head: T) (tail: (List T)) : (List T) = - ~λP λcons λnil (cons head tail) +cons +- head: T +- tail: (List T) +: (List T) + +~λP λcons λnil (cons head tail) diff --git a/book/List/drop.kind2 b/book/List/drop.kind2 index c8dbbe84..ef0afd69 100644 --- a/book/List/drop.kind2 +++ b/book/List/drop.kind2 @@ -1,11 +1,15 @@ use List/{cons,nil} use Nat/{succ,zero} -drop (n: Nat) (list: (List A)) : (List A) = - match n { - zero: list - succ: match list { - cons: (drop _ n.pred list.tail) - nil: (nil _) - } +drop +- n: Nat +- list: (List A) +: (List A) + +match n { + zero: list + succ: match list { + cons: (drop _ n.pred list.tail) + nil: (nil _) } +} diff --git a/book/List/filter.kind2 b/book/List/filter.kind2 index 06b8e365..5cdaa4da 100644 --- a/book/List/filter.kind2 +++ b/book/List/filter.kind2 @@ -1,11 +1,15 @@ use List/{cons,nil} use Bool/{true,false} -filter (cond: A -> Bool) (list: (List A)) : (List A) = - match list { - nil: (nil _) - cons: match result = (cond list.head) { - true: (cons _ list.head (filter _ cond list.tail)) - false: (filter _ cond list.tail) - } +filter +- cond: A -> Bool +- list: (List A) +: (List A) + +match list { + nil: (nil _) + cons: match result = (cond list.head) { + true: (cons _ list.head (filter _ cond list.tail)) + false: (filter _ cond list.tail) } +} diff --git a/book/List/find.kind2 b/book/List/find.kind2 index 86d55110..add3cd75 100644 --- a/book/List/find.kind2 +++ b/book/List/find.kind2 @@ -2,11 +2,15 @@ use Bool/{true,false} use List/{cons,nil} use Maybe/{some,none} -find (cond: A -> Bool) (xs: (List A)) : (Maybe A) = - match xs { - cons: match result = (cond xs.head) { - true: (some _ xs.head) - false: (find _ cond xs.tail) - } - nil: (none _) +find +- cond: A -> Bool +- xs: (List A) +: (Maybe A) + +match xs { + cons: match result = (cond xs.head) { + true: (some _ xs.head) + false: (find _ cond xs.tail) } + nil: (none _) +} diff --git a/book/List/fold.kind2 b/book/List/fold.kind2 index 65846e43..05a3f05c 100644 --- a/book/List/fold.kind2 +++ b/book/List/fold.kind2 @@ -1,7 +1,12 @@ use List/{cons,nil} -List/fold (P: *) (c: A -> P -> P) (n: P) (xs: (List A)) : P = - match xs { - cons: (c xs.head (List/fold _ P c n xs.tail)) - nil: n - } +List/fold (P: *) +- c: A -> P -> P +- n: P +- xs: (List A) +: P + +match xs { + cons: (c xs.head (List/fold _ P c n xs.tail)) + nil: n +} diff --git a/book/List/length.kind2 b/book/List/length.kind2 index 3baf4dc7..55956c21 100644 --- a/book/List/length.kind2 +++ b/book/List/length.kind2 @@ -1,8 +1,11 @@ use List/{cons,nil} use Nat/{succ,zero} -length (xs: (List A)) : Nat = - match xs { - cons: (succ (length _ xs.tail)) - nil: zero - } +length +- xs: (List A) +: Nat + +match xs { + cons: (succ (length _ xs.tail)) + nil: zero +} diff --git a/book/List/map.kind2 b/book/List/map.kind2 index 7f31aae1..2d0ec481 100644 --- a/book/List/map.kind2 +++ b/book/List/map.kind2 @@ -1,7 +1,11 @@ use List/{cons,nil} -map (xs: (List A)) (f: A -> B) : (List B) = - fold xs { - cons: (cons _ (f xs.head) xs.tail) - nil: (nil _) - } +map +- xs: (List A) +- fn: A -> B +: (List B) + +fold xs { + cons: (cons _ (fn xs.head) xs.tail) + nil: (nil _) +} diff --git a/book/List/match.kind2 b/book/List/match.kind2 index cc3f348f..005c5eb7 100644 --- a/book/List/match.kind2 +++ b/book/List/match.kind2 @@ -1,7 +1,8 @@ match - (P: (List A) -> *) - (c: ∀(head: A) ∀(tail: (List A)) (P (List/cons A head tail))) - (n: (P (List/nil A))) - (xs: (List A)) -: (P xs) = - (~xs P c n) +- P: (List A) -> * +- c: ∀(head: A) ∀(tail: (List A)) (P (List/cons A head tail)) +- n: (P (List/nil A)) +- xs: (List A) +: (P xs) + +(~xs P c n) diff --git a/book/List/nil.kind2 b/book/List/nil.kind2 index 1128c069..54ae8324 100644 --- a/book/List/nil.kind2 +++ b/book/List/nil.kind2 @@ -1,2 +1,4 @@ -nil : (List T) = - ~λP λcons λnil nil +nil +: (List T) + +~λP λcons λnil nil diff --git a/book/List/or.kind2 b/book/List/or.kind2 index aa3fb3a7..d6add0c6 100644 --- a/book/List/or.kind2 +++ b/book/List/or.kind2 @@ -1,8 +1,11 @@ use List/{cons,nil} use Bool/{false} -or (list: (List Bool)) : Bool = - fold list { - cons: (Bool/or list.head list.tail) - nil: false - } +or +- list: (List Bool) +: Bool + +fold list { + cons: (Bool/or list.head list.tail) + nil: false +} diff --git a/book/List/reverse.kind2 b/book/List/reverse.kind2 index fc469174..ca8a4404 100644 --- a/book/List/reverse.kind2 +++ b/book/List/reverse.kind2 @@ -1,10 +1,17 @@ use List/{cons,nil} -reverse/go (list: (List A)) (result: (List A)) : (List A) = - match list { - nil: result - cons: (reverse/go _ list.tail (cons _ list.head result)) - } +reverse/go +- list: (List A) +- result: (List A) +: (List A) -reverse (list: (List A)) : (List A) = - (reverse/go _ list (nil _)) +match list { + nil: result + cons: (reverse/go _ list.tail (cons _ list.head result)) +} + +reverse +- list: (List A) +: (List A) + +(reverse/go _ list (nil _)) diff --git a/book/List/sum.kind2 b/book/List/sum.kind2 index 4cef644d..4d062c14 100644 --- a/book/List/sum.kind2 +++ b/book/List/sum.kind2 @@ -1,5 +1,8 @@ -sum (xs: (List U48)): U48 = - match xs { - ++: (+ xs.head (sum xs.tail)) - []: 0 - } +sum +- xs: (List U48) +: U48 + +match xs { + ++: (+ xs.head (sum xs.tail)) + []: 0 +} diff --git a/book/List/take.kind2 b/book/List/take.kind2 index 1f828223..faf05b36 100644 --- a/book/List/take.kind2 +++ b/book/List/take.kind2 @@ -1,11 +1,15 @@ use List/{cons,nil} use Nat/{succ,zero} -take (n: Nat) (list: (List A)) : (List A) = - match n { - zero: (nil _) - succ: match list { - cons: (cons _ list.head (take _ n.pred list.tail)) - nil: (nil _) - } +take +- n: Nat +- list: (List A) +: (List A) + +match n { + zero: (nil _) + succ: match list { + cons: (cons _ list.head (take _ n.pred list.tail)) + nil: (nil _) } +} diff --git a/book/List/zip.kind2 b/book/List/zip.kind2 index c2693157..00424fcc 100644 --- a/book/List/zip.kind2 +++ b/book/List/zip.kind2 @@ -1,10 +1,14 @@ use List/{cons,nil} -zip (as: (List A)) (bs: (List B)) : (List (Pair A B)) = - match as { - cons: match bs { - cons: (cons _ (Pair/new _ _ as.head bs.head) (zip _ _ as.tail bs.tail)) - nil: (nil _) - } +zip +- as: (List A) +- bs: (List B) +: (List (Pair A B)) + +match as { + cons: match bs { + cons: (cons _ (Pair/new _ _ as.head bs.head) (zip _ _ as.tail bs.tail)) nil: (nil _) } + nil: (nil _) +} diff --git a/book/Maybe/bind.kind2 b/book/Maybe/bind.kind2 index 573034bc..22f20915 100644 --- a/book/Maybe/bind.kind2 +++ b/book/Maybe/bind.kind2 @@ -1,7 +1,11 @@ use Maybe/{some,none} -bind (ma: (Maybe A)) (f: A -> (Maybe B)) : (Maybe B) = - match ma { - some: (f ma.value) - none: (none _) - } +bind +- ma: (Maybe A) +- f: A -> (Maybe B) +: (Maybe B) + +match ma { + some: (f ma.value) + none: (none _) +} diff --git a/book/Maybe/match.kind2 b/book/Maybe/match.kind2 index 6e835477..0604811d 100644 --- a/book/Maybe/match.kind2 +++ b/book/Maybe/match.kind2 @@ -1,7 +1,8 @@ match - (P: (Maybe A) -> *) - (s: ∀(value: A) (P (Maybe/some A value))) - (n: (P (Maybe/none A))) - (ma: (Maybe A)) -: (P ma) = - (~ma P s n) +- P: (Maybe A) -> * +- s: ∀(value: A) (P (Maybe/some A value)) +- n: (P (Maybe/none A)) +- ma: (Maybe A) +: (P ma) + +(~ma P s n) diff --git a/book/Maybe/monad.kind2 b/book/Maybe/monad.kind2 index c1c14f9c..e6fef2a8 100644 --- a/book/Maybe/monad.kind2 +++ b/book/Maybe/monad.kind2 @@ -1,2 +1,4 @@ -Maybe/monad : (Monad Maybe) = - (Monad/new _ Maybe/bind Maybe/pure) +Maybe/monad +: (Monad Maybe) + +(Monad/new _ Maybe/bind Maybe/pure) diff --git a/book/Maybe/none.kind2 b/book/Maybe/none.kind2 index c98c4816..54157a36 100644 --- a/book/Maybe/none.kind2 +++ b/book/Maybe/none.kind2 @@ -1,2 +1,4 @@ -none : (Maybe T) = - ~λP λsome λnone none +none +: (Maybe T) + +~λP λsome λnone none diff --git a/book/Maybe/pure.kind2 b/book/Maybe/pure.kind2 index d927c4e7..f95c62db 100644 --- a/book/Maybe/pure.kind2 +++ b/book/Maybe/pure.kind2 @@ -1,2 +1,5 @@ -pure (x: T) : (Maybe T) = - (Maybe/some _ x) +pure +- x: T +: (Maybe T) + +(Maybe/some _ x) diff --git a/book/Maybe/some.kind2 b/book/Maybe/some.kind2 index d1901015..0f7fde15 100644 --- a/book/Maybe/some.kind2 +++ b/book/Maybe/some.kind2 @@ -1,2 +1,5 @@ -some (value: T) : (Maybe T) = - ~λP λsome λnone (some value) +some +- value: T +: (Maybe T) + +~λP λsome λnone (some value) diff --git a/book/Monad/new.kind2 b/book/Monad/new.kind2 index 9380b938..3be3c9c3 100644 --- a/book/Monad/new.kind2 +++ b/book/Monad/new.kind2 @@ -3,6 +3,7 @@ new ∀(bind: ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B)) (M B)) ∀(pure: ∀(A: *) ∀(a: A) (M A)) (Monad M) -= λM λbind λpure - ~λP λnew - (new bind pure) + +λM λbind λpure +~λP λnew +(new bind pure) diff --git a/book/Nat/add.kind2 b/book/Nat/add.kind2 index f6509c95..8802af72 100644 --- a/book/Nat/add.kind2 +++ b/book/Nat/add.kind2 @@ -1,7 +1,11 @@ use Nat/{succ,zero} -add (a: Nat) (b: Nat) : Nat = - match a { - succ: (succ (add a.pred a)) - zero: b - } +add +- a: Nat +- b: Nat +: Nat + +match a { + succ: (succ (add a.pred b)) + zero: b +} diff --git a/book/Nat/double.kind2 b/book/Nat/double.kind2 index ee8fbd1f..c86edfcd 100644 --- a/book/Nat/double.kind2 +++ b/book/Nat/double.kind2 @@ -1,7 +1,10 @@ use Nat/{succ,zero} -double (n: Nat) : Nat = - match n { - zero: zero - succ: (succ (succ (double n.pred))) - } +double +- n: Nat +: Nat + +match n { + zero: zero + succ: (succ (succ (double n.pred))) +} diff --git a/book/Nat/equal.kind2 b/book/Nat/equal.kind2 index 14254d15..980c61ef 100644 --- a/book/Nat/equal.kind2 +++ b/book/Nat/equal.kind2 @@ -1,14 +1,18 @@ use Nat/{succ,zero} use Bool/{true,false} -equal (a: Nat) (b: Nat) : Bool = - match a with (b: Nat) { - succ: match b { - succ: (equal a.pred b.pred) - zero: false - } - zero: match b { - succ: false - zero: true - } +equal +- a: Nat +- b: Nat +: Bool + +match a with (b: Nat) { + succ: match b { + succ: (equal a.pred b.pred) + zero: false } + zero: match b { + succ: false + zero: true + } +} diff --git a/book/Nat/half.kind2 b/book/Nat/half.kind2 index 0ee388f7..ccd224b0 100644 --- a/book/Nat/half.kind2 +++ b/book/Nat/half.kind2 @@ -1,10 +1,13 @@ use Nat/{succ,zero} -half (n: Nat) : Nat = - match n { - succ: match n.pred { - succ: (succ (half n.pred.pred)) - zero: zero - } +half +- n: Nat +: Nat + +match n { + succ: match n.pred { + succ: (succ (half n.pred.pred)) zero: zero } + zero: zero +} diff --git a/book/Nat/is_gtn.kind2 b/book/Nat/is_gtn.kind2 index 66b60958..96019451 100644 --- a/book/Nat/is_gtn.kind2 +++ b/book/Nat/is_gtn.kind2 @@ -1,11 +1,15 @@ use Nat/{succ,zero} use Bool/{true,false} -is_gtn (a: Nat) (b: Nat) : Bool = - match a with (b: Nat) { - zero: false - succ: match b { - zero: true - succ: (is_gtn a.pred b.pred) - } +is_gtn +- a: Nat +- b: Nat +: Bool + +match a with (b: Nat) { + zero: false + succ: match b { + zero: true + succ: (is_gtn a.pred b.pred) } +} diff --git a/book/Nat/is_ltn.kind2 b/book/Nat/is_ltn.kind2 index f7117b68..70e0332e 100644 --- a/book/Nat/is_ltn.kind2 +++ b/book/Nat/is_ltn.kind2 @@ -1,14 +1,18 @@ use Nat/{succ,zero} use Bool/{true,false} -is_ltn (a: Nat) (b: Nat) : Bool = - match a with (b: Nat) { - zero: match b { - zero: false - succ: true - } - succ: match b { - zero: false - succ: (is_ltn a.pred b.pred) - } +is_ltn +- a: Nat +- b: Nat +: Bool + +match a with (b: Nat) { + zero: match b { + zero: false + succ: true } + succ: match b { + zero: false + succ: (is_ltn a.pred b.pred) + } +} diff --git a/book/Nat/is_ltn_or_eql.kind2 b/book/Nat/is_ltn_or_eql.kind2 index 60cf4680..79b8ad91 100644 --- a/book/Nat/is_ltn_or_eql.kind2 +++ b/book/Nat/is_ltn_or_eql.kind2 @@ -1,8 +1,12 @@ use Nat/{succ,zero} use Bool/{true,false} -is_ltn_or_eql (a: Nat) (b: Nat) : Bool = - match is_lt = (Nat/is_ltn a b) { - true: true - false: (Nat/equal a b) - } +is_ltn_or_eql +- a: Nat +- b: Nat +: Bool + +match is_lt = (Nat/is_ltn a b) { + true: true + false: (Nat/equal a b) +} diff --git a/book/Nat/is_zero.kind2 b/book/Nat/is_zero.kind2 index 32e41e1d..81aa5958 100644 --- a/book/Nat/is_zero.kind2 +++ b/book/Nat/is_zero.kind2 @@ -1,8 +1,11 @@ use Nat/{zero,succ} use Bool/{true,false} -is_zero (n: Nat) : Bool = - match n { - zero: true - succ: false - } +is_zero +- n: Nat +: Bool + +match n { + zero: true + succ: false +} diff --git a/book/Nat/match.kind2 b/book/Nat/match.kind2 index 13c213e1..220c1ee0 100644 --- a/book/Nat/match.kind2 +++ b/book/Nat/match.kind2 @@ -1,8 +1,8 @@ match - (P: Nat -> *) - (s: ∀(pred: Nat) (P (Nat/succ pred))) - (z: (P Nat/zero)) - (n: Nat) -: (P n) = - (~n P s z) - +- P: Nat -> * +- s: ∀(pred: Nat) (P (Nat/succ pred)) +- z: (P Nat/zero) +- n: Nat +: (P n) + +(~n P s z) diff --git a/book/Nat/mul.kind2 b/book/Nat/mul.kind2 index 53a6f782..27ab8925 100644 --- a/book/Nat/mul.kind2 +++ b/book/Nat/mul.kind2 @@ -1,7 +1,11 @@ use Nat/{succ,zero} -mul (a: Nat) (b: Nat) : Nat = - match b { - succ: (Nat/add a (Nat/mul a b.pred)) - zero: zero - } +mul +- a: Nat +- b: Nat +: Nat + +match b { + succ: (Nat/add a (Nat/mul a b.pred)) + zero: zero +} diff --git a/book/Nat/succ.kind2 b/book/Nat/succ.kind2 index 183b1b2a..7248ad33 100644 --- a/book/Nat/succ.kind2 +++ b/book/Nat/succ.kind2 @@ -1,2 +1,5 @@ -succ (n: Nat) : Nat = - ~λP λsucc λzero (succ n) +succ +- n: Nat +: Nat + +~λP λsucc λzero (succ n) diff --git a/book/Nat/zero.kind2 b/book/Nat/zero.kind2 index 00e97a0b..a4862326 100644 --- a/book/Nat/zero.kind2 +++ b/book/Nat/zero.kind2 @@ -1,2 +1,4 @@ -zero : Nat = - ~λP λsucc λzero zero +zero +: Nat + +~λP λsucc λzero zero diff --git a/book/Parser/bind.kind2 b/book/Parser/bind.kind2 index a60a0025..14472c90 100644 --- a/book/Parser/bind.kind2 +++ b/book/Parser/bind.kind2 @@ -1,8 +1,12 @@ use Parser/Result/{done,fail} -bind (pa: (Parser A)) (f: A -> (Parser B)) : (Parser B) = - λcode - match result = (pa code) { - done: (f result.value result.code) - fail: (fail _ result.error) - } +bind +- pa: (Parser A) +- f: A -> (Parser B) +: (Parser B) + +λcode + match result = (pa code) { + done: (f result.value result.code) + fail: (fail _ result.error) + } diff --git a/book/Parser/char.kind2 b/book/Parser/char.kind2 index 5867b082..9d982995 100644 --- a/book/Parser/char.kind2 +++ b/book/Parser/char.kind2 @@ -1,9 +1,11 @@ use Parser/Result/{done,fail} use List/{cons,nil} -char : (Parser Char) = - λcode - match code { - cons: (done _ code.tail code.head) - nil: (fail _ "eof") - } +char +: (Parser Char) + +λcode + match code { + cons: (done _ code.tail code.head) + nil: (fail _ "eof") + } diff --git a/book/Parser/decimal.kind2 b/book/Parser/decimal.kind2 index 98e09286..7c24f2c2 100644 --- a/book/Parser/decimal.kind2 +++ b/book/Parser/decimal.kind2 @@ -1,5 +1,7 @@ use Char/{is_decimal} use Parser/pick_while -decimal : (Parser String) = - (pick_while is_decimal) +decimal +: (Parser String) + +(pick_while is_decimal) diff --git a/book/Parser/fail.kind2 b/book/Parser/fail.kind2 index d2b241eb..3fa39f9a 100644 --- a/book/Parser/fail.kind2 +++ b/book/Parser/fail.kind2 @@ -1,2 +1,5 @@ -fail (error: String) : (Parser A) = - λcode (Parser/Result/fail _ error) +fail +- error: String +: (Parser A) + +λcode (Parser/Result/fail _ error) diff --git a/book/Parser/is_eof.kind2 b/book/Parser/is_eof.kind2 index 960da741..221c5c0d 100644 --- a/book/Parser/is_eof.kind2 +++ b/book/Parser/is_eof.kind2 @@ -2,9 +2,11 @@ use Parser/Result/{done} use Bool/{true,false} use List/{cons,nil} -is_eof : (Parser Bool) = - λcode - match code { - cons: (done _ code false) - nil: (done _ (nil _) true) - } +is_eof +: (Parser Bool) + +λcode + match code { + cons: (done _ code false) + nil: (done _ (nil _) true) + } diff --git a/book/Parser/map.kind2 b/book/Parser/map.kind2 index b4b4a16d..340f418a 100644 --- a/book/Parser/map.kind2 +++ b/book/Parser/map.kind2 @@ -1,8 +1,12 @@ use Parser/Result/{done,fail} -map (f: A -> B) (p: (Parser A)) : (Parser B) = - λcode - match result = (p code) { - done: (done _ result.code (f result.value)) - fail: (fail _ result.error) - } +map +- f: A -> B +- p: (Parser A) +: (Parser B) + +λcode + match result = (p code) { + done: (done _ result.code (f result.value)) + fail: (fail _ result.error) + } diff --git a/book/Parser/name.kind2 b/book/Parser/name.kind2 index d6973c39..432df838 100644 --- a/book/Parser/name.kind2 +++ b/book/Parser/name.kind2 @@ -1,5 +1,7 @@ use Char/{is_name} use Parser/pick_while -name : (Parser String) = - (pick_while is_name) +name +: (Parser String) + +(pick_while is_name) diff --git a/book/Parser/oper.kind2 b/book/Parser/oper.kind2 index b5663054..50d7d3c8 100644 --- a/book/Parser/oper.kind2 +++ b/book/Parser/oper.kind2 @@ -1,5 +1,7 @@ use Char/{is_oper} use Parser/pick_while -oper : (Parser String) = - (pick_while is_oper) +oper +: (Parser String) + +(pick_while is_oper) diff --git a/book/Parser/pick.kind2 b/book/Parser/pick.kind2 index 5149b697..f2d944f5 100644 --- a/book/Parser/pick.kind2 +++ b/book/Parser/pick.kind2 @@ -1,9 +1,11 @@ use Parser/Result/{done,fail} use List/{cons,nil} -pick : (Parser Char) = - λcode - match code { - cons: (done _ code.tail code.head) - nil: (fail _ "empty") - } +pick +: (Parser Char) + +λcode + match code { + cons: (done _ code.tail code.head) + nil: (fail _ "empty") + } diff --git a/book/Parser/pure.kind2 b/book/Parser/pure.kind2 index 86c80902..a9536537 100644 --- a/book/Parser/pure.kind2 +++ b/book/Parser/pure.kind2 @@ -1,2 +1,5 @@ -pure (value: A) : (Parser A) = - λcode (Parser/Result/done _ code value) +pure +- value: A +: (Parser A) + +λcode (Parser/Result/done _ code value) diff --git a/book/Parser/repeat.kind2 b/book/Parser/repeat.kind2 index f45047e2..05bdcc66 100644 --- a/book/Parser/repeat.kind2 +++ b/book/Parser/repeat.kind2 @@ -3,11 +3,15 @@ use Parser/pure use List/{cons,nil} use Nat/{succ,zero} -repeat (n: Nat) (p: (Parser A)) : (Parser (List A)) = - match n { - zero: (pure _ (nil _)) - succ: - (bind _ _ p (λhead - (bind _ _ (repeat _ n.pred p) (λtail - (pure _ (cons _ head tail)))))) - } +repeat +- n: Nat +- p: (Parser A) +: (Parser (List A)) + +match n { + zero: (pure _ (nil _)) + succ: + (bind _ _ p (λhead + (bind _ _ (repeat _ n.pred p) (λtail + (pure _ (cons _ head tail)))))) +} diff --git a/book/Parser/skip.kind2 b/book/Parser/skip.kind2 index 30950b3c..7675f8fb 100644 --- a/book/Parser/skip.kind2 +++ b/book/Parser/skip.kind2 @@ -1,2 +1,5 @@ -skip (parser: (Parser A)) : (Parser A) = - λcode (parser code) +skip +- parser: (Parser A) +: (Parser A) + +λcode (parser code) diff --git a/book/Parser/take.kind2 b/book/Parser/take.kind2 index 5b332570..6a7ec866 100644 --- a/book/Parser/take.kind2 +++ b/book/Parser/take.kind2 @@ -1,5 +1,8 @@ use Parser/repeat use Parser/char -take (n: Nat) : (Parser String) = - (repeat _ n char) +take +- n: Nat +: (Parser String) + +(repeat _ n char) diff --git a/book/Parser/test.kind2 b/book/Parser/test.kind2 index 30f7d185..5f7b9572 100644 --- a/book/Parser/test.kind2 +++ b/book/Parser/test.kind2 @@ -5,22 +5,24 @@ use Parser/Result/{done,fail} use Bool/{true,false} use Char/{equal} -test (test_str: String) : (Parser Bool) = - λcode - match test_str { - cons: - match code { - cons: - match eq = (equal test_str.head code.head) { - true: - match result = (test test_str.tail code.tail) { - done: (done _ code result.value) - fail: (fail _ result.error) - } - false: (done _ code false) - } - nil: (done _ code false) - } - nil: (done _ code true) - } +test +- test_str: String +: (Parser Bool) +λcode + match test_str { + cons: + match code { + cons: + match eq = (equal test_str.head code.head) { + true: + match result = (test test_str.tail code.tail) { + done: (done _ code result.value) + fail: (fail _ result.error) + } + false: (done _ code false) + } + nil: (done _ code false) + } + nil: (done _ code true) + } diff --git a/book/Parser/text.kind2 b/book/Parser/text.kind2 index cd28ef9a..815720a5 100644 --- a/book/Parser/text.kind2 +++ b/book/Parser/text.kind2 @@ -7,14 +7,17 @@ use Parser/fail use Bool/{true,false} use String/{length} -text (txt: String) : (Parser Unit) = - (skip _ - (bind _ _ (test txt) λsuccess - match success { - true: - (bind _ _ (take (length txt)) λx - (pure _ Unit/new)) - false: (fail _ "Text mismatch") - } - ) +text +- txt: String +: (Parser Unit) + +(skip _ + (bind _ _ (test txt) λsuccess + match success { + true: + (bind _ _ (take (length txt)) λx + (pure _ Unit/new)) + false: (fail _ "Text mismatch") + } ) +) diff --git a/book/Parser/until.kind2 b/book/Parser/until.kind2 index d6e00ee5..5bfaa365 100644 --- a/book/Parser/until.kind2 +++ b/book/Parser/until.kind2 @@ -1,5 +1,9 @@ use Parser/until/go use List/{nil} -until (until: (Parser Bool)) (parse: (Parser A)) : (Parser (List A)) = - (go _ until parse (nil _)) +until +- until: (Parser Bool) +- parse: (Parser A) +: (Parser (List A)) + +(go _ until parse (nil _)) diff --git a/book/Parser/variant.kind2 b/book/Parser/variant.kind2 index 2414e00d..4282e343 100644 --- a/book/Parser/variant.kind2 +++ b/book/Parser/variant.kind2 @@ -4,13 +4,16 @@ use Parser/bind use Parser/fail use Bool/{true,false} -variant (variants: (List (Parser/Guard A))) : (Parser A) = - match variants { - cons: - (bind _ _ (fst _ _ variants.head) λsuccess - match success { - true: (snd _ _ variants.head) - false: (variant _ variants.tail) - }) - nil: (fail _ "No matching variant") - } +variant +- variants: (List (Parser/Guard A)) +: (Parser A) + +match variants { + cons: + (bind _ _ (fst _ _ variants.head) λsuccess + match success { + true: (snd _ _ variants.head) + false: (variant _ variants.tail) + }) + nil: (fail _ "No matching variant") +} diff --git a/book/Sigma/new.kind2 b/book/Sigma/new.kind2 index a64945e7..e7372727 100644 --- a/book/Sigma/new.kind2 +++ b/book/Sigma/new.kind2 @@ -1,4 +1,5 @@ Sigma/new : ∀(A: *) ∀(B: ∀(x: A) *) ∀(a: A) ∀(b: (B a)) (Sigma A B) -= λA λB λa λb ~λP λnew (new a b) + +λA λB λa λb ~λP λnew (new a b) diff --git a/book/String/begin.kind2 b/book/String/begin.kind2 index d7f81a29..dc60a291 100644 --- a/book/String/begin.kind2 +++ b/book/String/begin.kind2 @@ -1,11 +1,14 @@ use List/{cons,nil} -begin (str: (List Char)) : (List Char) = - match str { - cons: - match str.tail { - cons: (cons _ str.head (begin str.tail)) - nil: str - } - nil: str - } +begin +- str: (List Char) +: (List Char) + +match str { + cons: + match str.tail { + cons: (cons _ str.head (begin str.tail)) + nil: str + } + nil: str +} diff --git a/book/String/cmp.kind2 b/book/String/cmp.kind2 index f748afca..aaf0f3cd 100644 --- a/book/String/cmp.kind2 +++ b/book/String/cmp.kind2 @@ -1,20 +1,21 @@ String/cmp : ∀(a: String) ∀(b: String) Cmp -= λa λb - use P = λx ∀(b: String) Cmp - use cons = λa.head λa.tail λb - use P = λx ∀(a.head: Char) ∀(a.tail: String) Cmp - use cons = λb.head λb.tail λa.head λa.tail - use P = λx Cmp - use ltn = Cmp/ltn - use eql = (cmp a.tail b.tail) - use gtn = Cmp/gtn - (~(U48/cmp a.head b.head) P ltn eql gtn) - use nil = λa.head λa.tail Cmp/gtn - (~b P cons nil a.head a.tail) - use nil = λb + +λa λb +use P = λx ∀(b: String) Cmp +use cons = λa.head λa.tail λb + use P = λx ∀(a.head: Char) ∀(a.tail: String) Cmp + use cons = λb.head λb.tail λa.head λa.tail use P = λx Cmp - use cons = λb.head λb.tail Cmp/ltn - use nil = Cmp/eql - (~b P cons nil) - (~a P cons nil b) + use ltn = Cmp/ltn + use eql = (cmp a.tail b.tail) + use gtn = Cmp/gtn + (~(U48/cmp a.head b.head) P ltn eql gtn) + use nil = λa.head λa.tail Cmp/gtn + (~b P cons nil a.head a.tail) +use nil = λb + use P = λx Cmp + use cons = λb.head λb.tail Cmp/ltn + use nil = Cmp/eql + (~b P cons nil) +(~a P cons nil b) diff --git a/book/String/concat.kind2 b/book/String/concat.kind2 index 69fa0d32..a1efc82f 100644 --- a/book/String/concat.kind2 +++ b/book/String/concat.kind2 @@ -1,4 +1,8 @@ use List/{concat} -concat (xs: (List Char)) (ys: (List Char)) : (List Char) = - (concat xs ys) +concat +- xs: (List Char) +- ys: (List Char) +: (List Char) + +(concat xs ys) diff --git a/book/String/cons.kind2 b/book/String/cons.kind2 index 2a0c3db9..ba260c54 100644 --- a/book/String/cons.kind2 +++ b/book/String/cons.kind2 @@ -1,2 +1,6 @@ -String/cons (head: Char) (tail: String) : String = - ~λP λcons λnil (cons head tail) +String/cons +- head: Char +- tail: String +: String + +~λP λcons λnil (cons head tail) diff --git a/book/String/equal.kind2 b/book/String/equal.kind2 index 43effb0d..f279dc93 100644 --- a/book/String/equal.kind2 +++ b/book/String/equal.kind2 @@ -1,17 +1,21 @@ -String/equal (a: String) (b: String) : Bool = - use P = λx ∀(b: String) Bool - use cons = λa.head λa.tail λb - use P = λx ∀(a.head: Char) ∀(a.tail: String) Bool - use cons = λb.head λb.tail λa.head λa.tail - (Bool/and - (U48/equal a.head b.head) - (String/equal a.tail b.tail) - ) - use nil = λa.head λa.tail Bool/false - (~b P cons nil a.head a.tail) - use nil = λb - use P = λx Bool - use cons = λb.head λb.tail Bool/false - use nil = Bool/true - (~b P cons nil) - (~a P cons nil b) +String/equal +- a: String +- b: String +: Bool + +use P = λx ∀(b: String) Bool +use cons = λa.head λa.tail λb + use P = λx ∀(a.head: Char) ∀(a.tail: String) Bool + use cons = λb.head λb.tail λa.head λa.tail + (Bool/and + (U48/equal a.head b.head) + (String/equal a.tail b.tail) + ) + use nil = λa.head λa.tail Bool/false + (~b P cons nil a.head a.tail) +use nil = λb + use P = λx Bool + use cons = λb.head λb.tail Bool/false + use nil = Bool/true + (~b P cons nil) +(~a P cons nil b) diff --git a/book/String/indent.kind2 b/book/String/indent.kind2 index f7f39e7f..bc72f675 100644 --- a/book/String/indent.kind2 +++ b/book/String/indent.kind2 @@ -1,7 +1,8 @@ indent : ∀(tab: Nat) String -= λtab - use P = λx String - use succ = λtab.pred (String/cons 32 (String/cons 32 (indent tab.pred))) - use zero = String/nil - (~tab P succ zero) + +λtab +use P = λx String +use succ = λtab.pred (String/cons 32 (String/cons 32 (indent tab.pred))) +use zero = String/nil +(~tab P succ zero) diff --git a/book/String/join.kind2 b/book/String/join.kind2 index 1d878d96..d56b53d3 100644 --- a/book/String/join.kind2 +++ b/book/String/join.kind2 @@ -1,15 +1,9 @@ -join (sep: String) (strs: (List String)) : String = - match strs { - List/cons: (String/concat strs.head (String/join/go sep strs.tail)) - List/nil: String/nil - } +join +- sep: String +- strs: (List String) +: String - - -//join -//: ∀(sep: String) ∀(strs: (List String)) String -//= λsep λstrs - //use P = λx String - //use cons = λh λt (String/concat h (String/join/go sep t)) - //use nil = String/nil - //(~strs P cons nil) +match strs { + List/cons: (String/concat strs.head (String/join/go sep strs.tail)) + List/nil: String/nil +} diff --git a/book/String/length.kind2 b/book/String/length.kind2 index 0b37f7c2..d6e228af 100644 --- a/book/String/length.kind2 +++ b/book/String/length.kind2 @@ -1,4 +1,7 @@ use List/{length} -length (s: (List Char)) : Nat = - (length s) +length +- s: (List Char) +: Nat + +(length s) diff --git a/book/String/newline.kind2 b/book/String/newline.kind2 index bdeb1b9c..5fc83d20 100644 --- a/book/String/newline.kind2 +++ b/book/String/newline.kind2 @@ -1,3 +1,4 @@ newline : String -= (String/cons 10 String/nil) + +(String/cons 10 String/nil) diff --git a/book/String/nil.kind2 b/book/String/nil.kind2 index 2950cb28..14d50cdf 100644 --- a/book/String/nil.kind2 +++ b/book/String/nil.kind2 @@ -1,2 +1,4 @@ -String/nil : String = - ~λP λcons λnil nil +String/nil +: String + +~λP λcons λnil nil diff --git a/book/String/quote.kind2 b/book/String/quote.kind2 index 20e24438..00994a16 100644 --- a/book/String/quote.kind2 +++ b/book/String/quote.kind2 @@ -1,4 +1,6 @@ use List/{cons,nil} -quote : (List Char) = - (cons _ '"' (nil _)) +quote +: (List Char) + +(cons _ '"' (nil _)) diff --git a/book/String/skip.kind2 b/book/String/skip.kind2 index b97124ce..7c9b59ac 100644 --- a/book/String/skip.kind2 +++ b/book/String/skip.kind2 @@ -1,23 +1,24 @@ skip : ∀(str: String) String -= λstr - use P = λx String - use cons = λc0 λcs + +λstr +use P = λx String +use cons = λc0 λcs + use P = λx ∀(c0: Char) ∀(cs: String) String + use true = λc0 λcs (String/skip cs) + use false = λc0 λcs use P = λx ∀(c0: Char) ∀(cs: String) String - use true = λc0 λcs (String/skip cs) - use false = λc0 λcs - use P = λx ∀(c0: Char) ∀(cs: String) String - use true = λc0 λcs - use P = λx ∀(c0: Char) String - use cons = λc1 λcs λc0 - use P = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) String - use true = λc0 λc1 λcs (String/skip/comment cs) - use false = λc0 λc1 λcs (String/cons c0 (String/cons c1 cs)) - (~(Char/is_slash c1) P true false c0 c1 cs) - use nil = λc0 (String/cons c0 String/nil) - (~cs P cons nil c0) - use false = λc0 λcs (String/cons c0 cs) - (~(Char/is_slash c0) P true false c0 cs) - (~(Char/is_blank c0) P true false c0 cs) - use nil = String/nil - (~str P cons nil) + use true = λc0 λcs + use P = λx ∀(c0: Char) String + use cons = λc1 λcs λc0 + use P = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) String + use true = λc0 λc1 λcs (String/skip/comment cs) + use false = λc0 λc1 λcs (String/cons c0 (String/cons c1 cs)) + (~(Char/is_slash c1) P true false c0 c1 cs) + use nil = λc0 (String/cons c0 String/nil) + (~cs P cons nil c0) + use false = λc0 λcs (String/cons c0 cs) + (~(Char/is_slash c0) P true false c0 cs) + (~(Char/is_blank c0) P true false c0 cs) +use nil = String/nil +(~str P cons nil) diff --git a/book/String/unpar.kind2 b/book/String/unpar.kind2 index 5324d681..81df805b 100644 --- a/book/String/unpar.kind2 +++ b/book/String/unpar.kind2 @@ -1,11 +1,12 @@ unpar : ∀(fst: Char) ∀(lst: Char) ∀(str: String) String -= λfst λlst λstr - use P = λx String - use cons = λhead λtail - use P = λx ∀(head: Char) ∀(tail: String) String - use true = λhead λtail (String/begin tail) - use false = λhead λtail (String/cons head tail) - (~(Char/equal head fst) P true false head tail) - use nil = String/nil - (~str P cons nil) + +λfst λlst λstr +use P = λx String +use cons = λhead λtail + use P = λx ∀(head: Char) ∀(tail: String) String + use true = λhead λtail (String/begin tail) + use false = λhead λtail (String/cons head tail) + (~(Char/equal head fst) P true false head tail) +use nil = String/nil +(~str P cons nil) diff --git a/book/String/wrap.kind2 b/book/String/wrap.kind2 index 5c364185..647baed1 100644 --- a/book/String/wrap.kind2 +++ b/book/String/wrap.kind2 @@ -1,2 +1,7 @@ -wrap (ini: String) (str: String) (end: String) : String = - (String/concat ini (String/wrap/go str end)) +wrap +- ini: String +- str: String +- end: String +: String + +(String/concat ini (String/wrap/go str end)) diff --git a/book/The/value.kind2 b/book/The/value.kind2 index 68df4493..1c869a05 100644 --- a/book/The/value.kind2 +++ b/book/The/value.kind2 @@ -1,2 +1,5 @@ -value (x: A) : (The A x) = - ~λP λvalue (value x) +value +- x: A +: (The A x) + +~λP λvalue (value x) diff --git a/book/Tree/fold.kind2 b/book/Tree/fold.kind2 index a3501d9a..f6e23a35 100644 --- a/book/Tree/fold.kind2 +++ b/book/Tree/fold.kind2 @@ -1,7 +1,12 @@ use Tree/{node,leaf} -Tree/fold (P: *) (nd: A -> P -> P -> P) (lf: P) (bm: (Tree A)) : P = - match bm with (nd: A -> P -> P -> P) (lf: P) { - node: (nd bm.val (Tree/fold _ P nd lf bm.lft) (Tree/fold _ P nd lf bm.rgt)) - leaf: lf - } +Tree/fold (P: *) +- nd: A -> P -> P -> P +- lf: P +- bm: (Tree A) +: P + +match bm with (nd: A -> P -> P -> P) (lf: P) { + node: (nd bm.val (Tree/fold _ P nd lf bm.lft) (Tree/fold _ P nd lf bm.rgt)) + leaf: lf +} diff --git a/book/Tree/gen.kind2 b/book/Tree/gen.kind2 index 66a4d32c..ca6ebfac 100644 --- a/book/Tree/gen.kind2 +++ b/book/Tree/gen.kind2 @@ -1,7 +1,11 @@ use Tree/{node,leaf} -gen (n: U48) (x: U48) : (Tree U48) = - switch n { - 0: (leaf _) - _: (node _ x (gen (- n 1) (+ (* x 2) 1)) (gen (- n 1) (+ (* x 2) 2))) - } +gen +- n: U48 +- x: U48 +: (Tree U48) + +switch n { + 0: (leaf _) + _: (node _ x (gen (- n 1) (+ (* x 2) 1)) (gen (- n 1) (+ (* x 2) 2))) +} diff --git a/book/Tree/leaf.kind2 b/book/Tree/leaf.kind2 index 424d6d2a..7697949d 100644 --- a/book/Tree/leaf.kind2 +++ b/book/Tree/leaf.kind2 @@ -1,3 +1,5 @@ -leaf : (Tree A) = - ~λP λnode λleaf - leaf +leaf +: (Tree A) + +~λP λnode λleaf +leaf diff --git a/book/Tree/match.kind2 b/book/Tree/match.kind2 index a864f24c..fda19e77 100644 --- a/book/Tree/match.kind2 +++ b/book/Tree/match.kind2 @@ -1,7 +1,8 @@ match - (P: (Tree A) -> *) - (n: ∀(val: A) ∀(lft: (Tree A)) ∀(rgt: (Tree A)) (P (Tree/node A val lft rgt))) - (l: (P (Tree/leaf A))) - (t: (Tree A)) -: (P t) = - (~t P n l) +- P: (Tree A) -> * +- n: ∀(val: A) ∀(lft: (Tree A)) ∀(rgt: (Tree A)) (P (Tree/node A val lft rgt)) +- l: (P (Tree/leaf A)) +- t: (Tree A) +: (P t) + +(~t P n l) diff --git a/book/Tree/node.kind2 b/book/Tree/node.kind2 index fa4d00e2..29e8b883 100644 --- a/book/Tree/node.kind2 +++ b/book/Tree/node.kind2 @@ -1,3 +1,8 @@ -node (val: A) (lft: (Tree A)) (rgt: (Tree A)) : (Tree A) = - ~λP λnode λleaf - (node val lft rgt) +node +- val: A +- lft: (Tree A) +- rgt: (Tree A) +: (Tree A) + +~λP λnode λleaf +(node val lft rgt) diff --git a/book/Tree/sum.kind2 b/book/Tree/sum.kind2 index 3a815782..3c1e705a 100644 --- a/book/Tree/sum.kind2 +++ b/book/Tree/sum.kind2 @@ -7,8 +7,11 @@ use Tree/{node,leaf} // / \ / \ (4) (9) // (1) (2) (3) (4) -sum (x: (Tree U48)) : U48 = - fold x { - node: (+ x.val (+ x.lft x.rgt)) - leaf: 0 - } +sum +- x: (Tree U48) +: U48 + +fold x { + node: (+ x.val (+ x.lft x.rgt)) + leaf: 0 +} diff --git a/book/U48/abs_diff.kind2 b/book/U48/abs_diff.kind2 index de629edc..ac98c155 100644 --- a/book/U48/abs_diff.kind2 +++ b/book/U48/abs_diff.kind2 @@ -1,8 +1,12 @@ use Bool/{true,false} -abs_diff (a: U48) (b: U48) : U48 = - let x = (U48/to_bool (< a b)) - match x { - true: (- b a) - false: (- a b) - } +abs_diff +- a: U48 +- b: U48 +: U48 + +let x = (U48/to_bool (< a b)) +match x { + true: (- b a) + false: (- a b) +} diff --git a/book/U48/cmp.kind2 b/book/U48/cmp.kind2 index 0a73a76c..22d779b0 100644 --- a/book/U48/cmp.kind2 +++ b/book/U48/cmp.kind2 @@ -1,4 +1,8 @@ -cmp (a: U48) (b: U48) : Cmp = - (U48/if/ (== a b) - (U48/if/ (< a b) Cmp/gtn Cmp/ltn) - Cmp/eql) +cmp +- a: U48 +- b: U48 +: Cmp + +(U48/if/ (== a b) + (U48/if/ (< a b) Cmp/gtn Cmp/ltn) + Cmp/eql) diff --git a/book/U48/equal.kind2 b/book/U48/equal.kind2 index f2e2fb4a..cf63277b 100644 --- a/book/U48/equal.kind2 +++ b/book/U48/equal.kind2 @@ -1,7 +1,11 @@ use Bool/{true,false} -equal (a: U48) (b: U48) : Bool = - switch x = (== a b) { - 0: false - _: true - } +equal +- a: U48 +- b: U48 +: Bool + +switch x = (== a b) { + 0: false + _: true +} diff --git a/book/U48/fib.kind2 b/book/U48/fib.kind2 index b553fd90..94c647ba 100644 --- a/book/U48/fib.kind2 +++ b/book/U48/fib.kind2 @@ -1,6 +1,9 @@ -fib (n: U48) : U48 = - switch n { - 0: 0 - 1: 1 - _: (+ (fib (- n 1)) (fib (- n 2))) - } +fib +- n: U48 +: U48 + +switch n { + 0: 0 + 1: 1 + _: (+ (fib (- n 1)) (fib (- n 2))) +} diff --git a/book/U48/from_nat.kind2 b/book/U48/from_nat.kind2 index 654c4cf0..27818925 100644 --- a/book/U48/from_nat.kind2 +++ b/book/U48/from_nat.kind2 @@ -1,7 +1,10 @@ use Nat/{succ,zero} -from_nat (n: Nat) : U48 = - match n { - succ: (+ 1 (from_nat n.pred)) - zero: 0 - } +from_nat +- n: Nat +: U48 + +match n { + succ: (+ 1 (from_nat n.pred)) + zero: 0 +} diff --git a/book/U48/if.kind2 b/book/U48/if.kind2 index 082feb16..fd30a335 100644 --- a/book/U48/if.kind2 +++ b/book/U48/if.kind2 @@ -1,5 +1,10 @@ -if

(x: U48) (t: P) (f: P) : P = - switch x { - 0: t - _: f - } +if

+- x: U48 +- t: P +- f: P +: P + +switch x { + 0: t + _: f +} diff --git a/book/U48/match.kind2 b/book/U48/match.kind2 index 2454cb51..55568677 100644 --- a/book/U48/match.kind2 +++ b/book/U48/match.kind2 @@ -1,5 +1,11 @@ -match (x: U48) (P: U48 -> *) (s: U48 -> (P (+ 1 x))) (z: (P 0)) : (P x) = - switch x { - 0: z - _: (s x-1) - }: (P x) +match +- x: U48 +- P: U48 -> * +- s: U48 -> (P (+ 1 x)) +- z: (P 0) +: (P x) + +switch x { + 0: z + _: (s x-1) +}: (P x) diff --git a/book/U48/max.kind2 b/book/U48/max.kind2 index 1c6da99f..49472944 100644 --- a/book/U48/max.kind2 +++ b/book/U48/max.kind2 @@ -1,5 +1,9 @@ -max (a: U48) (b: U48) : U48 = - switch x = (< a b) { - 0: a - _: b - } +max +- a: U48 +- b: U48 +: U48 + +switch x = (< a b) { + 0: a + _: b +} diff --git a/book/U48/min.kind2 b/book/U48/min.kind2 index 05173918..18dfafa5 100644 --- a/book/U48/min.kind2 +++ b/book/U48/min.kind2 @@ -1,5 +1,9 @@ -min (a: U48) (b: U48) : U48 = - switch x = (< a b) { - 0: b - _: a - } +min +- a: U48 +- b: U48 +: U48 + +switch x = (< a b) { + 0: b + _: a +} diff --git a/book/U48/show.kind2 b/book/U48/show.kind2 index 1db71e78..de790315 100644 --- a/book/U48/show.kind2 +++ b/book/U48/show.kind2 @@ -1,2 +1,5 @@ -U48/show (n: U48) : String = - (String/Chunk/build (U48/show/go n)) +U48/show +- n: U48 +: String + +(String/Chunk/build (U48/show/go n)) diff --git a/book/U48/sum.kind2 b/book/U48/sum.kind2 index 2ffc041a..d0a06cbe 100644 --- a/book/U48/sum.kind2 +++ b/book/U48/sum.kind2 @@ -1,5 +1,8 @@ -sum (n: U48) : U48 = - switch n { - 0: 0 - _: (+ n (sum n-1)) - } +sum +- n: U48 +: U48 + +switch n { + 0: 0 + _: (+ n (sum n-1)) +} diff --git a/book/U48/to_bool.kind2 b/book/U48/to_bool.kind2 index efa06f22..2dd1e447 100644 --- a/book/U48/to_bool.kind2 +++ b/book/U48/to_bool.kind2 @@ -1,7 +1,10 @@ use Bool/{true,false} -to_bool (x: U48) : Bool = - switch x { - 0: false - _: true - }: Bool +to_bool +- x: U48 +: Bool + +switch x { + 0: false + _: true +}: Bool diff --git a/book/Unit/match.kind2 b/book/Unit/match.kind2 index 442683b8..c3597003 100644 --- a/book/Unit/match.kind2 +++ b/book/Unit/match.kind2 @@ -1,4 +1,7 @@ match - (x: Unit) (P: Unit -> *) (new: (P Unit/new)) +- x: Unit +- P: Unit -> * +- new: (P Unit/new) : (P x) -= (~x P new) + +(~x P new) diff --git a/book/Unit/new.kind2 b/book/Unit/new.kind2 index d7e58250..f3b7aee9 100644 --- a/book/Unit/new.kind2 +++ b/book/Unit/new.kind2 @@ -1,2 +1,3 @@ -Unit/new : Unit = - ~λP λone one +Unit/new : Unit + +~λP λone one diff --git a/book/Vector/concat.kind2 b/book/Vector/concat.kind2 index 08a34a52..c2ea2b42 100644 --- a/book/Vector/concat.kind2 +++ b/book/Vector/concat.kind2 @@ -1,22 +1,14 @@ use Vector/{cons,nil} use Nat/{succ,zero,add} -concat (xs_len: Nat) (ys_len: Nat) - (xs: (Vector T xs_len)) - (ys: (Vector T ys_len)) +concat +- xs_len: Nat +- ys_len: Nat +- xs: (Vector T xs_len) +- ys: (Vector T ys_len) : (Vector T (add xs_len ys_len)) -= match xs { - cons: (cons (add xs.len ys_len) xs.head (concat xs.len ys_len xs.tail ys)) - nil: ys - } -//concat -//: ∀(T: *) - //∀(xs_len: Nat) ∀(xs: (Vector T xs_len)) - //∀(ys_len: Nat) ∀(ys: (Vector T ys_len)) - //(Vector T (add xs_len ys_len)) -//= λT λxs_len λxs λys_len λys - //(~xs _ - //λxs.len λxs.head λxs.tail - //(Vector.cons T (Nat.add xs.len ys_len) xs.head (concat T xs.len xs.tail ys_len ys)) - //ys) +match xs { + cons: (cons _ (add xs.len ys_len) xs.head (concat _ xs.len ys_len xs.tail ys)) + nil: ys +}: (Vector T (add xs.len ys_len)) diff --git a/book/Vector/cons.kind2 b/book/Vector/cons.kind2 index a9431260..801b4d25 100644 --- a/book/Vector/cons.kind2 +++ b/book/Vector/cons.kind2 @@ -1,2 +1,7 @@ -cons (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat/succ len)) = - ~ λP λcons λnil (cons len head tail) +cons +- len: Nat +- head: T +- tail: (Vector T len) +: (Vector T (Nat/succ len)) + +~ λP λcons λnil (cons len head tail) diff --git a/book/Vector/nil.kind2 b/book/Vector/nil.kind2 index a01c6134..f3e93c85 100644 --- a/book/Vector/nil.kind2 +++ b/book/Vector/nil.kind2 @@ -1,2 +1,4 @@ -nil : (Vector T Nat/zero) = - ~λP λcons λnil nil +nil +: (Vector T Nat/zero) + +~λP λcons λnil nil diff --git a/book/test.kind2 b/book/test.kind2 index 4e4e0224..c3aeb034 100644 --- a/book/test.kind2 +++ b/book/test.kind2 @@ -1 +1,4 @@ -test : (List U48) = [50, 60] +test +: (List U48) + +[50, 60] diff --git a/src/book/parse.rs b/src/book/parse.rs index e70cff37..dfcf0997 100644 --- a/src/book/parse.rs +++ b/src/book/parse.rs @@ -71,9 +71,14 @@ impl<'i> KindParser<'i> { // Arguments (optional) let mut args = im::Vector::new(); let mut uses = uses.clone(); - while self.peek_one() == Some('<') || self.peek_one() == Some('(') { - let implicit = self.peek_one() == Some('<'); - self.consume(if implicit { "<" } else { "(" })?; + while self.peek_one() == Some('<') || self.peek_one() == Some('(') || self.peek_one() == Some('~') || self.peek_one() == Some('-') { + let implicit = self.peek_one() == Some('<') || self.peek_one() == Some('~'); + let closing = self.peek_one() == Some('<') || self.peek_one() == Some('('); + if closing { + self.consume(if implicit { "<" } else { "(" })?; + } else { + self.consume(if implicit { "~" } else { "-" })?; + } let arg_name = self.parse_name()?; self.skip_trivia(); let arg_type = if self.peek_one() == Some(':') { @@ -82,7 +87,9 @@ impl<'i> KindParser<'i> { } else { Term::Met {} }; - self.consume(if implicit { ">" } else { ")" })?; + if closing { + self.consume(if implicit { ">" } else { ")" })?; + } uses = shadow(&arg_name, &uses); args.push_back((implicit, arg_name, arg_type)); self.skip_trivia(); @@ -100,8 +107,13 @@ impl<'i> KindParser<'i> { ann = false; } - // Value (mandatory) - self.consume("=")?; + // Optional '=' sign + self.skip_trivia(); + if self.peek_one() == Some('=') { + self.consume("=")?; + self.skip_trivia(); + } + let mut val = self.parse_term(fid, &uses)?; //println!("PARSING {}", nam); diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index 581fdc7d..17e96e15 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -879,7 +879,7 @@ impl Term { for (idx_name, _) in adt.idxs.iter().rev() { motive = Term::Lam { era: false, - nam: idx_name.clone(), + nam: format!("{}.{}", mat.name, idx_name), bod: Box::new(motive), }; }