§ Lean4 Dev Meeting

§ Macro

-- | do the iff.rfl as well.
macro_rules | `(tactic| rfl => `(tactic| exact Iff.rfl)

§ How to collate info?

§ Mapsto arrow

§ ext tactic

§ colGt

  x -- parsed as part of `x`.
  y -- parsed as part of `y`.
z -- is not parsed as part of `x y`.
ext (x
 y) -- should parse.

§ ppSpace

§ Scoped syntax

§ Trivia

§ Tactic development: Trace

-- Tactic.lean
import Lean
open Lean Meta Elab

syntax (name := trace) "trace " term : tactic

elab "foo" : tactic => do
  -- `TacticM Unit` expected
  logInfo "hi"

open Lean Meta Elab Tactic ~=
open Lean
open Lean.Meta
open Lean.Elab
open Lean.Elab.Tactic
elab "foo" : tactic => do
  logInfo "hi"
elab tk:"foo" val:term : tactic => do
  withRef tk (logInfo val)

§ Reducible

To clarify, @ [reducible ] marks the definition as reducible for typeclass inference specifically. By default typeclass inference avoids reducing because it would make the search very expensive.