initial syntax guide

SYNTAX.md

@@ -0,0 +1,149 @@
+# Kind2 Syntax Guide
+
+Kind2 is a minimal proof language based on the calculus of constructions, extended with self-types.
+This guide has been generated by Sonnet-3.5 and will be reviewed soon.
+
+## Basic Syntax
+
+### Comments
+- Single-line comments: `// Comment`
+
+### Simple Datatype Declarations
+```kind2
+data Nat
+| zero
+| succ (pred: Nat)
+```
+
+### Polymorphic Datatypes
+```kind2
+data List <T>
+| cons (head: T) (tail: (List T))
+| nil
+```
+
+### Dependent Types
+```kind2
+data Equal <A: Type> (a: A) (b: A)
+| refl (a: A) : (Equal A a a)
+
+data Sigma <A: Type> <B: A -> Type>
+| new (fst: A) (snd: (B fst))
+```
+
+### Function Definitions and Calls
+Functions in Kind2 use Lisp-like call syntax, requiring parentheses:
+The matched variable's fields are automatically added to the scope:
+```kind2
+add (a: Nat) (b: Nat) : Nat =
+  match a {
+    zero: b
+    succ: (succ (add a.pred b))
+  }
+
+// Function call
+(add (succ zero) (succ (succ zero)))
+```
+
+## Advanced Features
+
+### Generic Functions
+```kind2
+List/fold <A> <B> (xs: (List A)) (c: A -> B -> B) (n: B) : B =
+  match xs {
+    ++: (c xs.head (List/fold xs.tail c n))
+    []: n
+  }
+```
+Note that `++` and `[]` are shortcuts for `List/cons` and `List/nil`.
+
+### Universal Quantification
+Use `∀` or `forall`:
+```kind2
+∀(A: Type) ∀(B: Type) ...
+```
+
+### Lambda Functions
+Use `λ` or `lambda`:
+```kind2
+λx (x + 1)
+```
+
+### Implicit Arguments
+Use `<>` for erased implicit arguments:
+```kind2
+id <T: Type> (x: T) : T = x
+```
+
+### Metavariables
+Represented by `_`, metavariables allow the compiler to fill parts of the program automatically:
+```kind2
+(id _ 7)  // The compiler will infer the type argument
+```
+
+### Named Holes
+Use `?name` for debugging and inspection. This will cause the context around the hole to be printed in the console:
+```kind2
+(function_call ?hole_name)
+```
+
+### Operators
+- Arithmetic: `+`, `-`, `*`, `/`, `%`
+- Comparison: `==`, `!=`, `<`, `<=`, `>`, `>=`
+- Logical: `&&`, `||`, `!`
+
+### Type Universe
+Use `Type` or `*` to denote the type of types
+
+### Module System
+Use dot notation for accessing module members:
+```kind2
+(List/map (Nat/add 1) my_list)
+```
+
+## Self Types
+
+Self types allow a type to access its typed value, bridging value and type levels.
+
+### Self Type Introduction
+Use `$` to introduce a self type:
+```kind2
+$(self: T) X
+```
+
+### Self Type Instantiation
+Use `~` to instantiate a self type:
+```kind2
+(~some_self_type_value)
+```
+
+### Self-Encoded Versions of Earlier Types
+
+#### List (Self-Encoded)
+```kind2
+List (A: *) : * =
+  $(self: (List A))
+  ∀(P: (List A) -> *)
+  ∀(cons: ∀(head: A) ∀(tail: (List A)) (P (List/cons/ A head tail)))
+  ∀(nil: (P (List/nil/ A)))
+  (P self)
+
+List/cons/ <A: *> (head: A) (tail: (List A)) : (List A) =
+  ~λP λcons λnil (cons head tail)
+
+List/nil/ <A: *> : (List A) =
+  ~λP λcons λnil nil
+```
+
+### Pattern Matching as Self-Instantiation
+Pattern matching desugars to self-instantiation of a λ-encoding:
+```kind2
+// This pattern match:
+match x {
+  nil: foo
+  cons: (bar x.head x.tail)
+}
+
+// Desugars to:
+(~x foo (λhead λtail (bar head tail)))
+```

book/List.kind2

@@ -1,3 +1,10 @@
 data List <T>
 | cons (head: T) (tail: (List T))
 | nil
+
+// List (A: *) : * =
+//   $(self: (List A))
+//   ∀(P: (List A) -> *)
+//   ∀(cons: ∀(head: A) ∀(tail: (List A)) (P (List/cons/ A head tail)))
+//   ∀(nil: (P (List/nil/ A)))
+//   (P self)