{"comment":{"url":"https://api.github.com/repos/agda/agda/comments/12426029","html_url":"https://github.com/agda/agda/commit/f45b4a2216281407a2c536b9961a1a501359a795#commitcomment-12426029","id":12426029,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"position":5,"line":621,"path":"src/full/Agda/Termination/Monad.hs","commit_id":"f45b4a2216281407a2c536b9961a1a501359a795","created_at":"2015-07-29T17:11:42Z","updated_at":"2015-07-29T17:11:42Z","body":"Why does it help to remove this \"do\" (and others below)?  Does it make the code more readable?  I think not.  Having a \"do\" here let's me easily introduce extra statements like debug printing without having to think whether the \"do\" is already present.  As a rule, I always put a \"do\" when starting a new block.  This is more robust than the other extreme, only putting \"do\"s when there are >=2 statements."}}