Proof Assistants Beta
Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze
  • Member for 1 year, 8 months
  • Last seen more than a month ago
Profile Activity
Stats
315
reputation
854
reached
4
answers
7
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
1
silver badge
7
bronze badges
Top tags
1
Score
9
Posts
82
Posts %
1
Score
9
Posts
82
Posts %
1
Score
2
Posts
18
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
question
8
Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
Mar 14, 2022
question
4
Is there a way in LeanProver to declare an inline recursive function, like fix in Coq?
Mar 7
question
2
unexpected inductive type occurrence error for recursive inductive type
Mar 12
answer
1
Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
Mar 27, 2022
answer
1
How to name the hypothesis resulting from the split tactic for if statements
Mar 7
question
1
Unravelling notations in Lean
Mar 10
question
1
How to prove pred_le_pred using tactics
Mar 7
question
1
How to name the hypothesis resulting from the split tactic for if statements
Mar 7
question
0
How to create an instance of TotalBLE
Mar 10
answer
0
How to create an instance of TotalBLE
Mar 12
Top network posts
View all network posts
14
Monadic Second Order Logic for Dummies

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.