767bda2c28
In the new code generator, we are going to lambda lift the instance methods before saving the code at the end of the base phase. The goal is to make instance ligth weight and cheap to inline. The anotation `@[inline]` is going to be an annotation for the lambda lifted methods. |
||
|---|---|---|
| .. | ||
| Control | ||
| Data | ||
| System | ||
| Classical.lean | ||
| Coe.lean | ||
| Control.lean | ||
| Conv.lean | ||
| Core.lean | ||
| Data.lean | ||
| Dynamic.lean | ||
| Hints.lean | ||
| Meta.lean | ||
| Notation.lean | ||
| NotationExtra.lean | ||
| Prelude.lean | ||
| ShareCommon.lean | ||
| SimpLemmas.lean | ||
| SizeOf.lean | ||
| SizeOfLemmas.lean | ||
| System.lean | ||
| Tactics.lean | ||
| Util.lean | ||
| WF.lean | ||
| WFTactics.lean | ||