Skip to content

Instantly share code, notes, and snippets.

View mn200's full-sized avatar
💭
Probably working on HOL

Michael Norrish mn200

💭
Probably working on HOL
70 followers · 1 following
View GitHub Profile
@mn200
mn200 / INSTALL-Z3-4.0.md
Created May 9, 2012 05:49
How to install Z3 4.0 on Linux

Installing Z3 version 4.0

  1. Download and unpack tar-ball from MSR download site.

  2. Run the z3 executable in z3/bin. Simple!

@mn200
mn200 / .gitignore
Created May 28, 2012 04:05
Getting things set up nicely for xmonad/xmobar/Ubuntu12.04
*.html
@mn200
mn200 / keybase.md
Created January 20, 2015 22:52

Keybase proof

I hereby claim:

  • I am mn200 on github.
  • I am michaeln (https://keybase.io/michaeln) on keybase.
  • I have a public key whose fingerprint is 1638 8636 37E5 313B 3BBF 5075 6286 43A7 A3DD 1D91

To claim this, I am signing this object:

@mn200
mn200 / HOL4 special assumptions (labels, abbreviations, etc).md
Last active February 1, 2025 01:30
Thoughts about assumption labelling (including hiding, abbreviation and protection)

Protecting Assumptions

Certain assumption types are naturally thought of being at least a bit protected. To be protected is to be somewhat immune to destructive changes.

“Destructive Changes”

Changes in Place: at the bottom level, there are relatively few facilities for changing assumptions in place other than with RULE_ASSUM_TAC. Of course, tactics can just access assumption lists directly, but most don't.