Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PairCases_on is undocumented #2

Closed
xrchz opened this issue Aug 28, 2011 · 1 comment
Closed

PairCases_on is undocumented #2

xrchz opened this issue Aug 28, 2011 · 1 comment
Labels
Bug Documentation

Comments

@xrchz
Copy link
Member

xrchz commented Aug 28, 2011

There is not even a helpful comment in the sig file (which is what you get from help "PairCases_on").
@mn200
Copy link
Member

mn200 commented Aug 28, 2011

I've assigned you to fix it (at least partially as a test of the issues tracker).

@ghost ghost assigned xrchz Aug 28, 2011
@xrchz xrchz closed this as completed in 8547380 Aug 30, 2011
acjf3 added a commit that referenced this issue Oct 18, 2011
@acjf3
Support for evaluating instructions of the form "ldr pc,[pc,rn,lsl #2]".
32efb82 
Previously this would not work for certain registers "rn".  This now works but a
precondition is added, namely: ARM_READ_REG rn state << 2 <> 0xFFFFFFF8w.
This ensures that the branch destination is not the machine-code value of the
instruction.
@xrchz xrchz mentioned this issue Mar 25, 2013
Closed
mn200 added a commit that referenced this issue Feb 26, 2014
@mn200
Allow prefix-operators to be printed without parens in rand-position
cf273a7 
This is a refinement to the decision in aeb0085, which insisted
that prefix operators (like if-then-else, binders, case-expressions
and others) should always get parentheses when printed as arguments to
functions.

Now you can tweak this by choosing the NotEvenIfRand parenthesis style
as an argument to add_rule. For particularly tight operators, ones
that may omit spaces before their arguments say, this may look better.
For example, you might define a "#" operator, when it might be nicer
to have

  f #2 + g #n

print that way, rather than with extra parentheses. At the moment, our
standard number injection function & does print with parentheses, but
this case does feel like one where dispensing with the parentheses
might be a good idea.
@xrchz xrchz removed their assignment Aug 7, 2014
mn200 added a commit that referenced this issue Nov 5, 2015
@mn200
Make type explicit to help mosml compilation
e78efa9 
It can't handle

   map #2 thms

if the type of thms isn't explicit at the function level.
binghe referenced this issue in binghe/HOL Aug 17, 2018
@binghe
Added more theorems for max/min into realTheory #2
2d45f18
binghe referenced this issue in binghe/HOL Aug 17, 2018
@binghe
Added more theorems for max/min into realTheory #2
ed6c48d
binghe referenced this issue in binghe/HOL Jan 19, 2019
@binghe
Fixed unicode_version of measure_absolutely_continuous #2
b11faa4
mn200 added a commit that referenced this issue Dec 10, 2019
@mn200
Use a type annotation to stop Moscow ML complaining about #2
5ae7764
oskarabrahamsson added a commit to oskarabrahamsson/HOL that referenced this issue May 13, 2023
@oskarabrahamsson
Remove cheat in example HOL-Theorem-Prover#2 proof
f4b7275
mn200 pushed a commit that referenced this issue Jul 20, 2023
@binghe @mn200
Hölder's and Minkowski's inequalities in the infinity cases #2
b23afc5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Bug Documentation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mn200 @xrchz