mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 19:27:42 +03:00
20 lines
1.2 KiB
Plaintext
20 lines
1.2 KiB
Plaintext
Kind.Term.parser.mat
|
|
: (Parser.Guard Kind.PreTerm)
|
|
= (Parser.Guard.text Kind.PreTerm "#match "
|
|
(Kind.Term.parser.bind Unit (Parser.text "#match ") λ_
|
|
(Kind.Term.parser.bind String Parser.name λnam
|
|
(Kind.Term.parser.bind Unit (Parser.text "=") λ_
|
|
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λx
|
|
(Kind.Term.parser.bind Unit (Parser.text "{") λ_
|
|
(Kind.Term.parser.bind Unit (Parser.text "#0") λ_
|
|
(Kind.Term.parser.bind Unit (Parser.text ":") λ_
|
|
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λz
|
|
(Kind.Term.parser.bind Unit (Parser.text "#+") λ_
|
|
(Kind.Term.parser.bind Unit (Parser.text ":") λ_
|
|
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λs
|
|
(Kind.Term.parser.bind Unit (Parser.text "}") λ_
|
|
(Kind.Term.parser.bind Unit (Parser.text ":") λ_
|
|
(Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λp
|
|
(Kind.Term.parser.pure λscp
|
|
(Kind.mat nam (x scp) (z scp) λx(s (Kind.Scope.extend (String.concat nam "-1") x scp)) λx(p (Kind.Scope.extend nam x scp)))))))))))))))))))
|