updated readme

README.org

@@ -6,6 +6,7 @@
 * Syntax
 The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. =λ= and =Π= abstractions can be written in the usual ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn't appear in the body as usual.
 
+** Terms
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 #+begin_src
   λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) ⇒ λ (y : β) ⇒ x
@@ -40,6 +41,7 @@ You can also directly bind functions. Here's an example.
 #+end_src
 The syntax for binding functions is just like with definitions.
 
+** Definitions and Axioms
 Definitions and axioms have abstract syntax as shown below.
 #+begin_src
   def <ident> (<ident> : <type>)* : <type>? := <term>;
@@ -57,6 +59,24 @@ Type ascriptions are optional in both definitions and =let= bindings. If include
 
 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.
 
+** Sections
+There is a Coq-like section mechanism. You open a section with =section <identifier>= and close it with =end <identifier>=. The identifiers used must match. The identifiers don't serve any purpose beyond organization.
+#+begin_src
+  section Test
+      variable (A B : *);
+      def id (x : A) := x;
+      def const (x : A) (y : B) := id x;
+  end Test
+
+  def id_full (A : *) (x : A) := id A x;
+  def const_full (A B : *) (x : A) (y : B) := const A B x y;
+#+end_src
+In a section, you can add section variables to the context with either =variable= or =hypothesis=. The syntax is the same as function parameters, so you can define multiple variables in one line, and can group section variables of the same type. Then, in the section, any definition using the section variables will be automatically generalized over the section variables that they use. Furthermore, any usage of such section variables (like =id x= in the definition of =const= above) will automatically apply the necessary section variables.
+
+Nested sections are supported, and work as you would expect.
+
+** Comments and preprocessor directives
+
 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.
 
 There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include <filepath>= (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. Additionally, =@include= automatically keeps track of what has been included, so duplicate inclusions are skipped, meaning no include guards are necessary.