%v: %s

" format show `to-int` : Tries to convert the top stack element to an integer, if possible. Interacting with the environment -------------------------------- `exit` : Exits the interpreter, immediately and unconditionally. `print` : Print the string at the top of the stack into the current document. `source` : Opens an external source file, and pushes a quote on the stack with its contents. `cache` : Given a resource name and a quote, does one of two things : - if the resource already exists, try to open it as a CaPriCon object, ignoring the quote - otherwise, run the quote and store its result in the resource for future use After the builtin has run, the contents of the requested object can be found at the top of the stack. `redirect` : Given a resource name and a quote, executes the quote, redirecting its output to the resource. String-Indexed Dictionaries --------------------------- `empty` : Pushes the empty dictionary onto the stack. `insert` : Given a dictionary `d`, a key `k` and a value `v`, inserts the value `v` at `k` in `d`, then pushes the result on the stack. `delete` : The reverse of `insert`. Given a dictionary `d` and a key `k`, produce a dictionary `d'` that is identical to `d`, without any association for `k`. `keys` : Given a dictionary `d`, pushes a list of all of `d`'s keys onto the stack. Constructing typed terms ----------------------- `universe` : Produces a universe. - `universe` : $i\ ...\ \rightarrow\ Set_i\ ...$ `variable` : Given a variable name, that exists in the current type context, produces that variable. - `variable` : $name\ ...\ \rightarrow\ var(name)\ ...$ `apply` : Given a function `f`, and a term `x`, produces the term `f x`. - `apply` : $x\ f\ ...\ \rightarrow\ (f\ x)\ ...$ `lambda` / `forall` : Abstracts the last hypothesis in context for the term at the top of the stack. That hypothesis is abstracted repectively as a lambda-abstraction, or a product. - `lambda` : $(\Gamma, h : T_h \vdash x)\ ... \rightarrow (\Gamma \vdash (\lambda (h : T_h). x))\ ...$ - `forall` : $(\Gamma, h : T_h \vdash x)\ ... \rightarrow (\Gamma \vdash (\forall (h : T_h), x))\ ...$ `mu` : Produces an inductive projection to a higher universe for the term at the top of the stack, if that term is of an inductive type. - `mu` : $x\ ...\ \rightarrow\ \mu(x)\ ...$ `axiom` : Given a combinatorial type (a type without free variables) and an associated tag, produce an axiom with that tag, that can serve as a proof of the given type. - `axiom` : $tag\ T\ ...\ \rightarrow\ Axiom_{T,tag}\ ...$ Analysing typed terms --------------------- `type` : Computes the type of the term at the top of the stack. `match` : Given a quote for each possible shape, and a term, executes the corresponding quote : - $k_{Set}\ k_{\lambda}\ k_{\forall}\ k_{apply}\ k_{\mu}\ k_{var}\ k_{axiom}$ `match` : - $|\ \Gamma \vdash (\lambda (x : T_x). y)\ ...\ \rightarrow\ k_{\lambda}(\Gamma, x : T_x \vdash\ x\ y\ ...)$ - $|\ \Gamma \vdash (\forall (x : T_x). y)\ ...\ \rightarrow\ k_{\forall}(\Gamma, x : T_x \vdash\ x\ y\ ...)$ - $|\ (f x_1..x_n)\ ...\ \rightarrow\ k_{apply}([x_1..x_n]\ f\ ...)$ - $|\ \mu(x)\ ...\ \rightarrow\ k_{\mu}(x\ ...)$ - $|\ x\ ...\ \rightarrow\ k_{var}(name(x)\ ...)$ - $|\ Axiom_{T,tag}\ ...\ \rightarrow\ k_{axiom}(tag\ T\ \ ...)$ - $|\ Set_n\ ...\ \rightarrow\ k_{Set}(n\ \ ...)$ `extract` : Extract the term at the top of the stack into an abstract algebraic representation, suitable for the production of foreign functional code, such as OCaml or Haskell. Managing the type context ------------------------- `intro` : Given a type $T$ and a name $H$, adds a new hypothesis $H$ of type $T$ to the context. Alternately, you can give a second hypothesis name $H'$, in which case the new hypothesis will be introduced before $H'$. `intro` : - $|\ \Gamma \vdash name(H)\ T\ ...\ \rightarrow \Gamma, H : T \vdash\ ...$ - $|\ \Gamma,H' : T_{H'},\Delta \vdash name(H')\ name(H)\ T\ ...\ \rightarrow \Gamma, H : T,H' : T_{H'},\Delta \vdash\ ...$ `extro-lambda` / `extro-forall` : Clears the last hypothesis from the context. Every term that references that hypothesis is abstracted either as a lambda-expression, or as a product, depending on the variant that was called. `rename` : Renames a hypothesis. This function takes two parameters : a hypothesis name, and the new name to give it. `substitute` : Given a hypothesis name, and a term of the same type as that hypothesis, remove that hypothesis from the context by substituting all its occurences by the given term. `hypotheses` : Pushes a list of all the hypotheses' names in context, from most recent to the oldest.