lean4-metaprogramming-book

lean4-metaprogramming-book copied to clipboard

The target of ?m3 should be f a = a.

pkshashank

In the original text, the choice of `m` is unfortunate, because `m` is already bound in the type. While the meaning is clear, it made me to trip and re-parse...

kustosz

Simple mistake in a worked example

kustosz

Adding exercises

1

## Progress - [ ] Introduction - [ ] Overview - [x] Expressions - [x] MetaM - [x] Metavariables - [x] Computation - [x] Constructing Epxressions - [x] Backtracking -...

lakesare

1. Inline code should be `more like this` 2. Some unicode symbols aren't getting rendered properly ___ Here is markdown on github for a comparison:

lakesare

bollu

ineol

I looked in lean-vscode for the relevant code to impl this but no luck. Since it's meant to be run interactively, why not elim a context switch? 

alok