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

chore: naming convetion

Browse source
This commit is contained in:
Leonardo de Moura 2021-11-25 08:05:03 -08:00
parent 8f88b1f3f8
commit 0de700fe45
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Declaration.lean
View file

@ -223,7 +223,7 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
@[export lean_inductive_val_is_reflexive] def InductiveVal.isReflexiveEx (v : InductiveVal) : Bool := v.isReflexive
@[export lean_inductive_val_is_nested] def InductiveVal.isNestedEx (v : InductiveVal) : Bool := v.isNested
def InductiveVal.nctors (v : InductiveVal) : Nat := v.ctors.length
def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
structure ConstructorVal extends ConstantVal where
induct : Name -- Inductive Type this Constructor is a member of

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

@ -26,7 +26,7 @@ private def isDefEqEtaStruct (a b : Expr) : MetaM Bool :=
return false
else
let inductVal ← getConstInfoInduct ctorVal.induct
if inductVal.nctors != 1 || inductVal.numIndices != 0 || inductVal.isRec then
if inductVal.numCtors != 1 || inductVal.numIndices != 0 || inductVal.isRec then
trace[Meta.isDefEq.eta.struct] "failed, type is not a structure{indentExpr b}"
return false
else if (← isDefEq (← inferType a) (← inferType b)) then