Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze
  • Member for 1 year, 11 months
  • Last seen more than a week ago
8 votes
2 answers
235 views

Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms

4 votes
1 answer
207 views

Is there a way in LeanProver to declare an inline recursive function, like fix in Coq?

2 votes
2 answers
116 views

unexpected inductive type occurrence error for recursive inductive type

1 vote
1 answer
202 views

Unravelling notations in Lean

1 vote
1 answer
65 views

How to prove pred_le_pred using tactics

1 vote
1 answer
116 views

How to name the hypothesis resulting from the split tactic for if statements

0 votes
2 answers
50 views

How to create an instance of TotalBLE