max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-18 07:47:28 -04:00
parent be11e8e29b
commit e8b58abdb2
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Meta/ExprDefEq.lean
View file

@ -1333,15 +1333,6 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
if tArgs.size < fvars.size then return none
return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
private def isSynthetic : Expr → MetaM Bool
| Expr.mvar mvarId => do
let mvarDecl ← getMVarDecl mvarId
match mvarDecl.kind with
| MetavarKind.synthetic => pure true
| MetavarKind.syntheticOpaque => pure true
| MetavarKind.natural => pure false
| _ => pure false
private def isAssignable : Expr → MetaM Bool
| Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
| _ => pure false