The only easy way to do this at the moment would be to
- Define a fake constant with the name of the binder you want, but which does
nothing. E.g.,
Define`AE x = x`;
- Make it a binder :
set_fixity “AE” Binder;
- Define your real constant as below:
Hi,
Suppose I have the following definition about a predicate P (with a measure
space m):
val almost_everywhere_def = Define `
almost_everywhere m P = ?N. null_set m N /\ !x. x IN (UNIV DIFF N) ==> P x`;
(I think you can safely think it as `almost_everywhere m P = !x. P x`.)
Now my
Second Call for Papers
WiL 2017: Women in Logic Workshop
Reykjavik, Iceland
June 19, 2017
https://sites.google.com/site/firstwomeninlogicworkshop/
NEW
* Submissions can be either a paper or a talk
