6 kyu
Drinker paradox
30 of 120yuxuanchiadm
Loading description...
Fundamentals
Theorem Proving
Mathematics
This comment has been reported as {{ abuseKindText }}.
Show
This comment has been hidden. You can view it now .
This comment can not be viewed.
- |
- Reply
- Edit
- View Solution
- Expand 1 Reply Expand {{ comments?.length }} replies
- Collapse
- Spoiler
- Remove
- Remove comment & replies
- Report
{{ fetchSolutionsError }}
-
-
Your rendered github-flavored markdown will appear here.
-
Label this discussion...
-
No Label
Keep the comment unlabeled if none of the below applies.
-
Issue
Use the issue label when reporting problems with the kata.
Be sure to explain the problem clearly and include the steps to reproduce. -
Suggestion
Use the suggestion label if you have feedback on how this kata can be improved.
-
Question
Use the question label if you have questions and/or need help solving the kata.
Don't forget to mention the language you're using, and mark as having spoiler if you include your solution.
-
No Label
- Cancel
Commenting is not allowed on this discussion
You cannot view this solution
There is no solution to show
Please sign in or sign up to leave a comment.
This comment has been hidden.
Lean Translation Kumited - please accept :-D
Approved
Coq translation https://www.codewars.com/kumite/5e3ea2cacc92260029e246d2?sel=5e3ea2cacc92260029e246d2
Thanks for your translation! I'm not familiar with Coq. So there is a little question. Is there a reason to have
rofnat -> Prop? Can this type be more general?natis just a random inhabited type. If you want to, I can change it to accept any inhabited type, but...Using
Set ℓisn't 'more general'; it's just weird.I mean, do you realize what you wrote meant? It was literally 'there is a type in universe level ℓ such that if this type is drinking, then every type in universe level ℓ is drinking'.
This comment has been hidden.
This comment has been hidden.