- localVar: Lean.Name → Lean.Elab.Term.PatternVar
- anonymousVar: Lean.MVarId → Lean.Elab.Term.PatternVar
Equations
- Lean.Elab.Term.instToStringPatternVar = { toString := fun x => match x with | Lean.Elab.Term.PatternVar.localVar x => toString x | Lean.Elab.Term.PatternVar.anonymousVar mvarId => toString "?m" ++ toString mvarId.name ++ toString "" }
Equations
- Lean.Elab.Term.getMVarSyntaxMVarId stx = { name := Lean.Syntax.getKind (Lean.Syntax.getOp stx 0) }
- found : Lean.NameSet
- vars : Array Lean.Elab.Term.PatternVar
@[inline]
- funId : Lean.Syntax
- ctorVal? : Option Lean.ConstructorVal
- explicit : Bool
- ellipsis : Bool
- paramDecls : Array (Lean.Name × Lean.BinderInfo)
- paramDeclIdx : Nat
- namedArgs : Array Lean.Elab.Term.NamedArg
- args : List Lean.Elab.Term.Arg
- newArgs : Array Lean.Syntax
Equations
- Lean.Elab.Term.CollectPatternVars.instInhabitedContext = { default := { funId := default, ctorVal? := default, explicit := default, ellipsis := default, paramDecls := default, paramDeclIdx := default, namedArgs := default, args := default, newArgs := default } }
partial def
Lean.Elab.Term.CollectPatternVars.collect.pushNewArg
(accessible : Bool)
(ctx : Lean.Elab.Term.CollectPatternVars.Context)
(arg : Lean.Elab.Term.Arg)
:
partial def
Lean.Elab.Term.CollectPatternVars.collect.processCtorAppCore
(f : Lean.Syntax)
(namedArgs : Array Lean.Elab.Term.NamedArg)
(args : Array Lean.Elab.Term.Arg)
(ellipsis : Bool)
:
Equations
- Lean.Elab.Term.CollectPatternVars.main alt = do let patterns ← Array.mapM (fun p => let cls := `Elab.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax := fun y => Lean.Elab.Term.CollectPatternVars.collect p if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "collecting variables at pattern: " ++ Lean.toMessageData p ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) alt.patterns pure { ref := alt.ref, patterns := patterns, rhs := alt.rhs }
Equations
- Lean.Elab.Term.collectPatternVars alt = do let discr ← StateRefT'.run (Lean.Elab.Term.CollectPatternVars.main alt) { found := ∅, vars := #[] } let x : Lean.Elab.Term.MatchAltView × Lean.Elab.Term.CollectPatternVars.State := discr match x with | (alt, s) => pure (s.vars, alt)
Equations
- Lean.Elab.Term.getPatternVars patternStx = do let patternStx ← Lean.Elab.liftMacroM (Lean.expandMacros patternStx) let discr ← StateRefT'.run (Lean.Elab.Term.CollectPatternVars.collect patternStx) { found := ∅, vars := #[] } let x : Lean.Syntax × Lean.Elab.Term.CollectPatternVars.State := discr match x with | (x, s) => pure s.vars
Equations
- Lean.Elab.Term.getPatternsVars patterns = let collect := do let r ← forIn patterns PUnit.unit fun pattern r => do let a ← Lean.Elab.liftMacroM (Lean.expandMacros pattern) discard (Lean.Elab.Term.CollectPatternVars.collect a) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit; do let discr ← StateRefT'.run collect { found := ∅, vars := #[] } let x : Unit × Lean.Elab.Term.CollectPatternVars.State := discr match x with | (x, s) => pure s.vars
Equations
- Lean.Elab.Term.getPatternVarNames pvars = Array.filterMap (fun x => match x with | Lean.Elab.Term.PatternVar.localVar x => some x | x => none) pvars 0 (Array.size pvars)