gebner
Follow
Pinned
1,819 contributions in the last year
Activity overview
Contributed to
leanprover/lean4,
leanprover-community/mathlib4,
leanprover-community/mathport
and 37 other
repositories
Contribution activity
February 2023
Created 17 commits in 4 repositories
Created a pull request in leanprover/lean4 that received 3 comments
fix: reenable structure eta during tc search
Fixes #2074 Structure eta is for TC instances is required to see that subobject projections are defeq with constructor applications. These diamonds…
+79
−7
•
3
comments
Opened 7 other pull requests in 4 repositories
leanprover-community/mathlib4
3
closed
leanprover/lean4
1
open
1
merged
leanprover/std4
1
merged
leanprover/vscode-lean4
1
merged
Reviewed 9 pull requests in 3 repositories
leanprover-community/mathlib4
6 pull requests
- [Merged by Bors] - chore: bump to leanprover/lean4:nightly-2023-02-10
- [Merged by Bors] - feat: port Topology.Order.Hom.Basic
- fix: fin bug in to_additive
- [Merged by Bors] - fix: interaction between to_additive and rewriting definitions
-
[Merged by Bors] - fix: use focus in
cases'andinduction' - feat: simps uses fields of parent structures
leanprover/lean4
2 pull requests
leanprover/std4
1 pull request
Created an issue in leanprover/lean4 that received 1 comment
Compiler error with subtypes of erased types
class Insert (α : outParam (Type u)) (β : Type v) where insert : α → β → β export Insert (insert) abbrev Set (α : Type u) := α → Prop instance : In…
1
comment