DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: LInt

Browse source
This commit is contained in:
jstoobysmith 2024-09-19 07:57:32 -04:00
parent 9bfbb24d29
commit fa4ab7f14f
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/Meta/Informal.lean
View file

@ -75,8 +75,8 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
dep_def? := some (← `([ $deps,* ]))
| `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
dep_def? := some (← `([$deps,*]))
| _ => Macro.throwError "invalid assignment syntax in informal_definition"
unless math_def?.isSome do
Macro.throwError "A 'math' assignments is required"
@ -115,8 +115,8 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
dep_def? := some (← `([ $deps,* ]))
| `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
dep_def? := some (← `([$deps,*]))
| _ => Macro.throwError "invalid assignment syntax"
unless math_def?.isSome do
Macro.throwError "A 'math' assignments is required"