1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
|
---input---
kind list type -> type.
type nil list A.
type cons A -> list A -> list A.
kind tm type.
type fun (tm -> tm) -> tm.
type app tm -> tm -> tm.
pred foo i:(tm -> tm), o:tm.
---tokens---
'kind' Keyword.Declaration
' ' Text.Whitespace
'list' Name.Function
' ' Text.Whitespace
'type' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'type' Keyword.Type
'.' Text
'\n' Text.Whitespace
'type' Keyword.Declaration
' ' Text.Whitespace
'nil' Name.Function
' ' Text.Whitespace
'list' Keyword.Type
' ' Text.Whitespace
'A' Keyword.Type
'.' Text
'\n' Text.Whitespace
'type' Keyword.Declaration
' ' Text.Whitespace
'cons' Name.Function
' ' Text.Whitespace
'A' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'list' Keyword.Type
' ' Text.Whitespace
'A' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'list' Keyword.Type
' ' Text.Whitespace
'A' Keyword.Type
'.' Text
'\n' Text.Whitespace
'kind' Keyword.Declaration
' ' Text.Whitespace
'tm' Name.Function
' ' Text.Whitespace
'type' Keyword.Type
'.' Text
'\n' Text.Whitespace
'type' Keyword.Declaration
' ' Text.Whitespace
'fun' Name.Function
' ' Text.Whitespace
'(' Keyword.Type
'tm' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'tm' Keyword.Type
')' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'tm' Keyword.Type
'.' Text
'\n' Text.Whitespace
'type' Keyword.Declaration
' ' Text.Whitespace
'app' Name.Function
' ' Text.Whitespace
'tm' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'tm' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'tm' Keyword.Type
'.' Text
'\n' Text.Whitespace
'pred' Keyword.Declaration
' ' Text.Whitespace
'foo' Name.Function
' ' Text.Whitespace
'i:' Keyword.Mode
'(' Keyword.Type
'tm' Keyword.Type
' ' Text.Whitespace
'->' Keyword.Type
' ' Text.Whitespace
'tm' Keyword.Type
')' Keyword.Type
',' Text
' ' Text.Whitespace
'o:' Keyword.Mode
'tm' Keyword.Type
'.' Text
'\n' Text.Whitespace
|