Leonardo de Moura 8db923e010 feat: generate error message for simp theorems that are equivalent to x = x ... see #973 see https://github.com/leanprover-community/mathport/issues/70		2022-01-26 11:16:31 -08:00
..
CongrLemmas.lean	refactor: avoid Name, MVarId, and FVarId confusion	2021-09-07 19:06:50 -07:00
Main.lean	fix: check "heartbeats" at simp	2022-01-26 07:50:25 -08:00
Rewrite.lean	fix: igore instance implicit arguments in term ordering used at simp	2022-01-24 18:57:31 -08:00
SimpAll.lean	refactor: simplify and document SimpLemma encoding	2021-04-10 15:03:04 -07:00
SimpLemmas.lean	feat: generate error message for simp theorems that are equivalent to x = x	2022-01-26 11:16:31 -08:00
Types.lean	feat: add environment extension for caching Simp.Context for splitIf	2021-08-16 13:05:01 -07:00