Incremental and intercepted parsing of Lean code #114

Open
opened 2024-10-13 17:50:45 -07:00 by aniva · 1 comment
Owner

The Putnam dataset has this:

import Mathlib
open BigOperators

open Topology Filter

abbrev putnam_2019_a1_solution : Set ℤ := sorry
-- {n : ℤ | n ≥ 0 ∧ ¬Int.ModEq 9 n 3 ∧ ¬Int.ModEq 9 n 6}
/--
Determine all possible values of the expression
\[
A^3+B^3+C^3-3ABC
\]
where $A, B$, and $C$ are nonnegative integers.
-/
theorem putnam_2019_a1
: {n : ℤ | ∃ A B C : ℤ, A ≥ 0 ∧ B ≥ 0 ∧ C ≥ 0 ∧ A^3 + B^3 + C^3 - 3*A*B*C = n} = putnam_2019_a1_solution :=
sorry

Suppose the abbrev line is commented out, it would be a useful feature to parse the theorem only and skip over the abbrev. Specifically we could let the user decide the fate of each compilation unit and give the user the choice to update the environment or not.

The Putnam dataset has this: ```lean import Mathlib open BigOperators open Topology Filter abbrev putnam_2019_a1_solution : Set ℤ := sorry -- {n : ℤ | n ≥ 0 ∧ ¬Int.ModEq 9 n 3 ∧ ¬Int.ModEq 9 n 6} /-- Determine all possible values of the expression \[ A^3+B^3+C^3-3ABC \] where $A, B$, and $C$ are nonnegative integers. -/ theorem putnam_2019_a1 : {n : ℤ | ∃ A B C : ℤ, A ≥ 0 ∧ B ≥ 0 ∧ C ≥ 0 ∧ A^3 + B^3 + C^3 - 3*A*B*C = n} = putnam_2019_a1_solution := sorry ``` Suppose the `abbrev` line is commented out, it would be a useful feature to parse the theorem only and skip over the abbrev. Specifically we could let the user decide the fate of each compilation unit and give the user the choice to update the environment or not.
aniva added the
part/Frontend
category
feature
labels 2024-10-13 17:50:45 -07:00
aniva self-assigned this 2024-10-13 17:50:45 -07:00
aniva added a new dependency 2024-10-21 11:24:12 -07:00
Author
Owner

Partly solved by #113

Partly solved by #113
Sign in to join this conversation.
No Milestone
No project
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Reference: aniva/Pantograph#114
No description provided.