{"push_id":651549913,"size":1,"distinct_size":1,"ref":"refs/heads/master","head":"118189eaacd1af7d6dfeb4450761e5a16ddb78f2","before":"e1dc18f6b6aad5dabc13cb9b93978c32f31e7939","commits":[{"sha":"118189eaacd1af7d6dfeb4450761e5a16ddb78f2","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(frontends/lean/elaborator): bug in translation function\n\nThis commit fixes the bug reported in the lean discussion list:\nhttps://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/118189eaacd1af7d6dfeb4450761e5a16ddb78f2"}]}