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

feat: add auxiliary constructions

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-24 08:46:35 -07:00
parent b5977d9c06
commit 53406bbc36
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/Structure.lean
View file

@ -429,6 +429,15 @@ match mkProjections env structName projs isClass with
| Except.ok env => setEnv env
| Except.error msg => throwError ref msg
private def mkAuxConstructions (declName : Name) : CommandElabM Unit := do
env ← getEnv;
let hasUnit := env.contains `PUnit;
let hasEq := env.contains `Eq;
let hasHEq := env.contains `HEq;
modifyEnv fun env => mkRecOn env declName;
when hasUnit $ modifyEnv fun env => mkCasesOn env declName;
when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declName
/-
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
@ -474,7 +483,7 @@ withDeclId declId $ fun name => do
let ref := declId;
addDecl ref r.decl;
addProjections ref declName r.projInfos isClass;
-- TODO: add auxiliary definitions recOn and casesOn
mkAuxConstructions declName;
-- TODO: register default values
-- TODO: add coercions
pure ()