{"comment":{"url":"https://api.github.com/repos/Blaisorblade/pts/comments/9674083","html_url":"https://github.com/Blaisorblade/pts/commit/9f8363ac8017dfdcf8ede065fb7f45368bed280f#commitcomment-9674083","id":9674083,"user":{"login":"Blaisorblade","id":289960,"avatar_url":"https://avatars.githubusercontent.com/u/289960?v=3","gravatar_id":"","url":"https://api.github.com/users/Blaisorblade","html_url":"https://github.com/Blaisorblade","followers_url":"https://api.github.com/users/Blaisorblade/followers","following_url":"https://api.github.com/users/Blaisorblade/following{/other_user}","gists_url":"https://api.github.com/users/Blaisorblade/gists{/gist_id}","starred_url":"https://api.github.com/users/Blaisorblade/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Blaisorblade/subscriptions","organizations_url":"https://api.github.com/users/Blaisorblade/orgs","repos_url":"https://api.github.com/users/Blaisorblade/repos","events_url":"https://api.github.com/users/Blaisorblade/events{/privacy}","received_events_url":"https://api.github.com/users/Blaisorblade/received_events","type":"User","site_admin":false},"position":null,"line":null,"path":"","commit_id":"9f8363ac8017dfdcf8ede065fb7f45368bed280f","created_at":"2015-02-10T12:37:19Z","updated_at":"2015-02-10T12:37:19Z","body":"Good point, I didn't, and this breaks `LindleyF.lpts`. But I think the offending bindings should be specially annotated in the source, and should be restricted to be used as macros (that is, forbidden from being abstract/postulates/etc., so that they can be normalized away). And we'd need to check a few things (probably boring ones) to see that they make sense."}}