michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/rewrite_loop): notation

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-04 19:21:26 -08:00
parent d0171ffe7a
commit 61a029d9df
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/rewrite_loop.lean
View file

@ -3,5 +3,5 @@ open algebra
theorem test {A : Type} [s : comm_ring A] (a b c : A) : a + b + c = a + c + b :=
begin
rewrite ?add.comm
rewrite *add.comm
end