def Lean.LocalDecl.setKind : Lean.LocalDecl → Lean.LocalDeclKind → Lean.LocalDecl

Set the kind of a LocalDecl.

Equations

• One or more equations did not get rendered due to their size.

def Lean.LocalContext.getRoundtrippingUserName? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Option Lean.Name

Given an FVarId, this function returns the corresponding user name, but only if the name can be used to recover the original FVarId.

Equations

• One or more equations did not get rendered due to their size.

def Lean.LocalContext.setKind (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (kind : Lean.LocalDeclKind) : Lean.LocalContext

Set the kind of the given fvar.

Equations

• Lean.LocalContext.setKind lctx fvarId kind = Lean.LocalContext.modifyLocalDecl lctx fvarId fun (x : Lean.LocalDecl) => Lean.LocalDecl.setKind x kind

def Lean.LocalContext.sortFVarsByContextOrder (lctx : Lean.LocalContext) (hyps : Array Lean.FVarId) : Array Lean.FVarId

Sort the given FVarIds by the order in which they appear in lctx. If any of the FVarIds do not appear in lctx, the result is unspecified.

Equations

• One or more equations did not get rendered due to their size.