diff --git a/HepLean/SpaceTime/LorentzTensor/Notation.lean b/HepLean/SpaceTime/LorentzTensor/Notation.lean index 45a61d9..de4024e 100644 --- a/HepLean/SpaceTime/LorentzTensor/Notation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Notation.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.LorentzTensor.Basic +import HepLean.SpaceTime.LorentzTensor.Real.Basic import Init.NotationExtra /-! @@ -68,4 +68,7 @@ def indexParser : ParserFn := (takeWhileFnFst (IsIndexSpecifier 𝓣) IsIndexId def indexParserMany : ParserFn := Lean.Parser.many1Fn (indexParser 𝓣) +def singleTensorElab : Lean.Elab.Term.TermElab := fun stx expectedType => do + return mkNatLit 0 + end IndexNotation