feat: Extract used constants from invocation #119

Merged
aniva merged 2 commits from frontend/data into dev 2024-11-10 21:29:35 -08:00
Owner
  • feat: Extract used constants from tactic invocation

e.g.

example : ∀ (p q: Prop), p → p ∨ q := by
  intro p q h
  exact Or.inl h

The second step uses the constant Or.inl h.

- feat: Extract used constants from tactic invocation e.g. ```lean example : ∀ (p q: Prop), p → p ∨ q := by intro p q h exact Or.inl h ``` The second step uses the constant `Or.inl h`.
aniva added this to the 0.2.20 milestone 2024-11-05 14:40:11 -08:00
aniva added the
part/Frontend
category
feature
labels 2024-11-05 14:40:11 -08:00
aniva self-assigned this 2024-11-05 14:40:11 -08:00
aniva added 1 commit 2024-11-05 14:40:12 -08:00
aniva added a new dependency 2024-11-05 14:40:28 -08:00
aniva added 1 commit 2024-11-08 14:52:09 -08:00
aniva merged commit 4f6ccd3e82 into dev 2024-11-10 21:29:35 -08:00
aniva deleted branch frontend/data 2024-11-10 21:29:35 -08:00
Sign in to join this conversation.
No description provided.