A tactic macro

4/4 ~30 minlean

Define a tactic macro that introduces all possible binders.

8 lines · Lean 4

import Lean

macro "intro_all" : tactic =>
  sorry

example (P Q : Prop) : P → Q → P := by
  intro_all
  assumption

Objectifs

Indices

Voir la solution

import Lean

macro "intro_all" : tactic =>
  `(tactic| repeat intro)

example (P Q : Prop) : P → Q → P := by
  intro_all
  assumption