Sebastian Ullrich
@kha.functional.cafe.ap.brid.gy
makes Lean at Lean FRO
Munich, Germany
[bridged from https://functional.cafe/@kha on the fediverse by https://fed.brid.gy/ ]
Munich, Germany
[bridged from https://functional.cafe/@kha on the fediverse by https://fed.brid.gy/ ]
One month, the introduction of a phase distinction, and various adjustments to the elaborator and codegen later, we have a first build short-circuiting on a trivial change to an executable `def`.
(before/after)
(before/after)
June 15, 2025 at 1:40 PM
One month, the introduction of a phase distinction, and various adjustments to the elaborator and codegen later, we have a first build short-circuiting on a trivial change to an executable `def`.
(before/after)
(before/after)