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
8 votes
2 answers
241 views

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

4 votes
1 answer
213 views

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

2 votes
2 answers
117 views

unexpected inductive type occurrence error for recursive inductive type

1 vote
1 answer
224 views

Unravelling notations in Lean

1 vote
1 answer
66 views

How to prove pred_le_pred using tactics

1 vote
1 answer
145 views

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

0 votes
2 answers
52 views

How to create an instance of TotalBLE