All Questions
5
questions
7
votes
2
answers
157
views
When is the lean 4 "by" required?
I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally ...
- 2,220
3
votes
2
answers
137
views
Lean4: How to construct an HEq between dependent functions?
I have an extremely simple goal to prove:
HEq
(fun px rd =>
match px, rd with
| Sum.inr _ppos, dir => dir)
fun x => id
The reason the match ...
- 41
4
votes
1
answer
1k
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 257
5
votes
1
answer
465
views
Tactics for Array/List simplification in lean4
Because there are both Arrays and Lists in Lean4, sometimes you end up with code that has a mixture of Lists and Arrays interspersed with basic operations and conversions between the two. For example,...
- 257
5
votes
1
answer
486
views
Simple Proof about `String.split`
I am new to lean, working on proving a simple lemma in lean4.
lemma String.split_empty (c): String.split "" c = [""]
I tried looking for ...
- 257