Lean Notes

Lean Notes

Table of Contents

1.	Metaprogramming Exercises
2.	Call-by-value evaluation with cbv
3.	Bird's determinant algorithm
	Index

2. Call-by-value evaluation with cbv

2.1.	Reducing functions defined via well-founded recursion
2.2.	Suppressing a definition with `@[cbv_opaque]`
2.3.	Using `cbv` with stdlib data structures

←1.2. Right-associative And (Anne's solution)2.1. Reducing functions defined via well-founded recursion→

2. Call-by-value evaluation with cbv🔗

This note records some examples of using cbv features.

2.1. Reducing functions defined via well-founded recursion
2.2. Suppressing a definition with @[cbv_opaque]
2.3. Using cbv with stdlib data structures

←1.2. Right-associative And (Anne's solution)2.1. Reducing functions defined via well-founded recursion→