Appendix D: Language reference index
Use the syntax quick reference for notation and the chapters below for explanations and examples. This index locates the rules covered by the book. It is not an exhaustive specification of every construct or an inventory of unverified features.
D.1 Values, declarations, and types
| Question | Rule and boundary | Explanation |
|---|---|---|
| Bindings and assignment | Distinguish let from var; use := to assign a mutable cell | Values and types |
| Numeric types | Do not equate fixed-width integers, floating-point values, and the proof-level Nat | Basic types, runtime correspondence |
| Functions and branches | Check parameter and result types, branch results, and remaining effects | Functions and control flow |
| Data structures | Distinguish struct fields, enum constructors, and match cases | Structs, enums, and match |
| Type parameters | The book uses <A> for function parameters and List(A) for type application. Do not extrapolate this to arbitrary term generics | Generics |
| Classes | Distinguish a where Ord(A) requirement, its comparison implementation, and laws used in proofs | Classes, sorting proofs |
| Names and imports | Check relative imports, standard-library imports, and visibility through pub | Projects |
D.2 Ownership, borrowing, and effects
| Question | Rule and boundary | Explanation |
|---|---|---|
copy / shared / affine / linear | Rules for duplication and disposal, separate from whether a variable is mutable | Ownership kinds |
& and &mut | Distinguish reading and mutable borrows from passing ownership of a value | Borrowing |
| View bindings | Check the usage scope of let &x := ... | Borrowing and references |
perform / handle | Separate requesting an effect from handling it; unhandled effects remain outside | Algebraic effects |
! {…} | Read externally visible effects separately from the function result | Functions, effects |
resume | Consider both continuation usage counts and the usage rules of captured values | Continuations and ownership |
| Budgets | Distinguish language budgets from host time and memory limits | Execution limits, trust boundary |
D.3 Propositions, proofs, and universes
| Question | Rule and boundary | Explanation |
|---|---|---|
Prop and proof terms | Read propositions as types and proofs as terms of those types | First proofs |
Refl | Use when both sides coincide through computation of their definitions, not as an automatic proof of arbitrary mathematical equality | Equality |
| Induction | Distinguish constructor cases from the induction hypothesis | Induction and recursion |
| Tactics | Distinguish assistance constructing a proof from checking the completed proof | Tactics |
?name | An unfinished hole; displaying a candidate does not replace checking the filled term | Proof tools |
Type(u) / Level | Read universe levels without assuming unrestricted inference of symbolic levels | Dependent types and universes |
| Axioms and external functions | Assumed propositions and external implementations are part of the trust boundary | Trust boundary |
D.4 Common distinctions
- Type conversion and equality proofs: definitional agreement during type checking is not the same operation as providing a proof term for an equality proposition. Equality that does not follow by computation may require rewriting or another proof.
- Theorems and execution tests: a theorem about general inputs and a test on selected inputs provide different evidence. Success in one does not imply success in the other.
- Dependent types and all type-level functions: being able to write a proposition containing values does not imply that every executable function or class method works in a type position. Check the intended path with a small example.
- Checked and executable: even after a file checks, separately verify its combination of backend, host capabilities, and external functions.
D.5 Looking beyond this index
Inspect exact standard API parameters and visibility with tauto library FILE and tauto doc PATH for the version you use. Consult tauto --help and each subcommand's --help for CLI options. Do not use this index as a complete specification of macros, FFI, or every backend constraint.
Instead of inventing missing syntax, make a small reproduction using the verification guide. Record proposed designs separately from functionality available in the distributed version.