Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze's user avatar
Walter Schulze
  • Member for 2 years, 1 month
  • Last seen more than a month ago
2 votes
2 answers
117 views

unexpected inductive type occurrence error for recursive inductive type

0 votes
2 answers
52 views

How to create an instance of TotalBLE

1 vote
1 answer
224 views

Unravelling notations in Lean

4 votes
1 answer
213 views

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

1 vote
1 answer
66 views

How to prove pred_le_pred using tactics

1 vote
1 answer
146 views

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

8 votes
2 answers
242 views

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