diff --git a/README.md b/README.md index d3ad1fb..e407b12 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ Type ascriptions are optional. If included, `perga` will check to make sure your If the RHS of a definition is `axiom`, then `perga` will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms. -Line comments are `--` like in Haskell, and block comments are `(* *)` like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish. +Line comments are `--` like in Haskell, and block comments are `[* *]` somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish. # Usage @@ -120,7 +120,7 @@ Obviously not fully decidable, but I might be able to implement some basic unifi ### TODO Implicits -Much, much more useful than [inference](#orgdba513b), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing. +Much, much more useful than [inference](#orgfd5754c), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing. ### TODO Module System @@ -130,7 +130,7 @@ A proper module system would be wonderful. To me, ML style modules with structur ### TODO Universes? -Not really all that necessary, especially without [inductive definitions](#org1f674ce), but could be fun. +Not really all that necessary, especially without [inductive definitions](#org3e4a465), but could be fun. ### TODO Inductive Definitions @@ -197,7 +197,7 @@ I’m imagining the parser could be chosen based on the file extension or so ### TODO treesitter parser and/or emacs mode -Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn’t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org4dd267a), to better handle indentation, automatically adjust line numbers, etc. +Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn’t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org461e006), to better handle indentation, automatically adjust line numbers, etc. ### TODO TUI diff --git a/README.org b/README.org index e4892bf..c394ac5 100644 --- a/README.org +++ b/README.org @@ -28,7 +28,7 @@ Type ascriptions are optional. If included, =perga= will check to make sure your If the RHS of a definition is =axiom=, then =perga= will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms. -Line comments are =--= like in Haskell, and block comments are =(* *)= like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish. +Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish. * Usage Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. Entering ":t " prints the type of a particular identifier. Entering ":n " will fully normalize (including unfolding definitions) an expression. diff --git a/lib/Parser.hs b/lib/Parser.hs index 1b54114..7c5eee9 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -49,7 +49,7 @@ skipSpace = L.space space1 (L.skipLineComment "--") - (L.skipBlockCommentNested "(*" "*)") + (L.skipBlockCommentNested "[*" "*]") lexeme :: Parser a -> Parser a lexeme = L.lexeme skipSpace