Daniel Selsam
Daniel Selsam
As several of us discussed the other day, the following may become increasingly problematic as proofs get bigger and use more automation: ```Lean begin tac1, -- expensive tac2 -- calling...
Many users have gotten confused and frustrated by the behavior of wildcards in the equation compiler. There is at least one open Github issue devoted to this discussion (https://github.com/leanprover/lean/issues/1466). The...
The C++ kernel is still more trustworthy than the reference type checker, so if the reference type checker fails to type check the standard library it is most likely an...
lighter-weight alternative to https://github.com/leanprover-community/mathport/pull/136 consistent with the changed export format in https://github.com/leanprover-community/lean/pull/702/commits/a8b8424c6dd64e2135661c6a580a397c3663b2e8
```lean import Mathlib.Analysis.NormedSpace.HahnBanach import Mathlib.PostPort namespace Real.Playground set_option synthInstance.maxHeartbeats 5000 universe u v w variable {E : Type u} [instSNG : SemiNormedGroup E] [instSNS : SemiNormedSpace ℝ E] variable (p...
The auto-name-translation maps e.g. `pgame` -> `Pgame`. There are many examples of this. Consider adding support for an extensible word-split list, e.g. mapping "pgame" to ["p", "game"].
Note: this issue was previously considered in the now-archived binport repo https://github.com/dselsam/binport/issues/8 (Binport-importing) typeclass queries are failing due to the discrimination tree indexing. Here is an example: ```lean import Mathlib.Analysis.NormedSpace.HahnBanach...