Naïm Camille Favier

@h7x4

Thanks. That leaves the issue of the mysterious `RDNS_NONE` which I can't reproduce using `rspamadm`: Full email including rspamd symbols ``` Return-Path: Delivered-To: [email protected] Received: from monade.li by mu with...

Here's what my postfix logs say around the time that email was received: ``` Jul 28 10:54:50 warning: numeric hostname: 54.240.48.106 Jul 28 10:54:50 connect from unknown[54.240.48.106] Jul 28 10:54:51...

I've managed to implement the macro suggested in the OP, with a few changes to Agda! [Here's the code and demo](https://github.com/ncfavier/1lab/blob/unbind/src/1Lab/Reflection/Unbind.agda), [here's the corresponding branch of Agda](https://github.com/agda/agda/commits/ncfavier/unbind). The basic idea...

Thanks, done. - https://github.com/agda/agda/pull/6568 - https://github.com/agda/agda/pull/6569 - https://github.com/agda/agda/pull/6570

Using the trick in https://github.com/agda/agda/issues/5738#issuecomment-1013295556 I was able to simplify my macros to not use tactic arguments, which also solves the issue with nesting. The code does not depend on...

> In standard mathematical notation (i.e, ∃ means _mere_ existence), we have ~~But in `agda-stdlib`, [`∃`](https://agda.github.io/agda-stdlib/Data.Product.Base.html#852) means `Σ`. Is that where the confusion is coming from?~~ ~~`Surjection` uses `Surjective`, which...

I did that; after rescanning, syncthing correctly showed the extra files as local additions, and after discarding them I am back to the exact same situation, which leads me to...

Nope, cannot reproduce in a new folder. :( In fact even with the music folder, if I delete a file from computer then it gets correctly deleted from phone, without...

I re-added the folder again with `fs`, `db` and `model` enabled; here are the lines of the log that mention just one of the ghost files: https://gist.github.com/ncfavier/00dc2c71afb34588e704b08458ea37da. Note in particular...