File tree Expand file tree Collapse file tree 2 files changed +16
-4
lines changed
Expand file tree Collapse file tree 2 files changed +16
-4
lines changed Original file line number Diff line number Diff line change 1- def string_xor : Unit :=
2- ()
1+ import Std.Data.Iterators
2+
3+ def stringXor (a b : List Bool) : List Bool :=
4+ ((a.iter).zip b.iter)
5+ |>.map (fun p => Bool.xor p.1 p.2 )
6+ |>.toList
7+
8+ @ [simp, grind]
9+ theorem length_stringXor {a b : List Bool} : (stringXor a b).length = min a.length b.length := by
10+ simp [stringXor]
11+
12+ theorem getElem_stringXor {a b : List Bool} {i : Nat} {hia : i < a.length} {hib : i < b.length} :
13+ (stringXor a b)[i]'(by grind) = Bool.xor a[i] b[i] := by
14+ simp [stringXor]
315
416/-!
517## Prompt
@@ -44,4 +56,4 @@ def check(candidate):
4456 assert candidate('1', '1') == '0'
4557 assert candidate('0101', '0000') == '0101'
4658```
47- -/
59+ -/
Original file line number Diff line number Diff line change 1- leanprover/lean4:nightly-2025-08-18
1+ leanprover/lean4:nightly-2025-06-11
You can’t perform that action at this time.
0 commit comments