{var%20f='http://v.t.sina.com.cn/share/share.php?appkey=1515056452',u=z||d.location,p=['&url=',e(u),'&title=',e(t||d.title),'&source=',e(r),'&sourceUrl=',e(l),'&content=',c||'gb2312','&pic=',e(p||'')].join('');function%20a(){if(!window.open([f,p].join(''),'mb',['toolbar=0,status=0,resizable=1,width=440,height=430,left=',(s.width-440)/2,',top=',(s.height-430)/2].join('')))u.href=[f,p].join('');};if(/Firefox/.test(navigator.userAgent))setTimeout(a,0);else%20a();})(screen,document,encodeURIComponent,'','','https://www.manongdao.com/data/attach/logo/logo.png', '推荐 兄弟一词,经得起流年. 的问题《Is there a way to disable a specific notation in C》','https://www.manongdao.com/q-782091.html','页面编码gb2312|utf-8默认gb2312'));){kind=link}
I'd like, in Coqide, to have the proof state not use a certain notation (but still use all others).
Is this possible?
相关问题
- Rewriting with John Major's equality
- Easier way to prevent numbers from showing in expo
- Can canonical structure resolution be interleaved
- Defining recursive function over product type
- coq: elimination of forall quantifier
相关文章
- coq error when trying to use Case. Example from So
- How to switch the current goal in Coq?
- What does “Error: Universe inconsistency” mean in
- A productive alternative to UML
- Coq - use Prop (True | False) in if … then … else
- Consistent formulations of sets in Coq?
- Different induction principles for Prop and Type
- Coq: Prop versus Set in Type(n)
Some tricks that might be sufficient are described here: How to disable my custom notation in Coq?
I wanted to add pointer to that answer because this question comes up first on Google.
From what I understand in the documentation, it is not possible. You might be able to play with opening/closing scopes but I'm not sure it will work, since it is stated explicitly that notations will be used for printing whenever possible.