Skip to main content
Proof Assistants Beta
HTNW's user avatar
HTNW's user avatar
HTNW's user avatar
HTNW
  • Member for 2 years, 3 months
  • Last seen this week
Profile Activity
Stats
573
reputation
3k
reached
7
answers
1
question
Communities
View all
Badges
View all badges
This user doesn’t have any gold badges yet.
2
silver badges
6
bronze badges
Top tags
View all tags
17
Score
5
Posts
62
Posts %
14
Score
3
Posts
38
Posts %
6
Score
1
Posts
12
Posts %
6
Score
1
Posts
12
Posts %
5
Score
1
Posts
12
Posts %
4
Score
1
Posts
12
Posts %
Top posts
9
What axioms do I need to search the naturals?
Apr 24, 2022
6
Cannot discriminate `0 = 1`
Apr 15, 2022
6
Defining and using bisimilarity for negatively-defined conatural numbers
Feb 17
5
Why do coinductive types require bisimilarity relations?
Jun 7, 2022
4
How do I convince the Lean 4 type checker that addition is commutative?
May 11, 2022
3
How to write if_then_else function that accepts a type argument explicitly?
Mar 10, 2023
3
What is a positive coinductive type and why are they so bad?
Jun 30
2
How to express that two equivalence relations can setoid rewrite across each other (Coq)
Nov 17, 2023
Top network posts
View all network posts
65
Accidentally did dd /dev/sda
61
How can a point source emit spherical EM waves when they are forbidden by Maxwell's equations?
45
If diverging rays never meet, why do parallel rays meet at infinity?
32
What is the difference between a partition name and a partition label?
28
Monad laws expressed in terms of join instead of bind?