Proof Assistants Beta
Jozef Mikušinec's user avatar
Jozef Mikušinec's user avatar
Jozef Mikušinec's user avatar
Jozef Mikušinec
  • Member for 1 year
  • Last seen more than a week ago
Profile Activity
Stats
267
reputation
1k
reached
0
answers
3
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
1
silver badge
6
bronze badges
Top tags
0
Score
3
Posts
100
Posts %
0
Score
2
Posts
67
Posts %
0
Score
1
Posts
33
Posts %
0
Score
1
Posts
33
Posts %
Top posts
All Questions Answers
Score Newest
question
11
Given `A = B`, how to prove `a: A` also has type B in Lean 4
Sep 17, 2022
question
3
Equality of records with members whose types are dependent (Lean 4)
Sep 21, 2022
question
2
(In Lean), why cannot structural recursion on propositions be used?
Sep 29, 2022
Top network posts
View all network posts
16
If A and B are correlated and A and C are correlated. Why is it possible for B and C to be uncorrelated?
10
What are the issues with a set-like interpretation of quantifiers in type theory?
6
An analogue of Scott continuity for infinite-time-Turing-computable functions

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.