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

chore: use double-backtick

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-05 10:28:57 -08:00
parent 210e2ba3bc
commit f080389c3f
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/Inductive.lean
View file

@ -430,10 +430,10 @@ private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTy
private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
let env ← getEnv
let hasEq := env.contains `Eq
let hasHEq := env.contains `HEq
let hasUnit := env.contains `PUnit
let hasProd := env.contains `Prod
let hasEq := env.contains ``Eq
let hasHEq := env.contains ``HEq
let hasUnit := env.contains ``PUnit
let hasProd := env.contains ``Prod
for view in views do
let n := view.declName
mkRecOn n