Custom Query (361 matches)

Hello, I tried proofgeneral on the newly released emacs and it works at first sight but seems to have some problems with long input, like the one produced by this bash script:

function mk { echo "Check fun n, match n with "; s=O; for ((i=0;i<$1;i++)); do 
echo "  | $s => n"; s="(S $s)"; done; echo "  | _ => n end."; } > x.v

Processing x.v for small arguments like $ mk 10 works but for bigger ones like $ mk 100 it blocks without consuming cpu. Weirdly for me the threshold seems to be 42...

ProofGeneral > Save Options doesn't make PG remember that "Unicode tokens" was set in a previous session. (This used to work previously.)

Paste the following code in. After the final period, press either Ctrl+J or enter followed by tab. Emacs (Aquamacs or GNU Emacs 23) will spin up one processor to 100% and run forever.

Theorem binaryUnaryCommute' : forall b : bin,
  convert (succ (b)) = convert b + 1.
Proof.
  intros b.
  induction b as [| b' | b'].
  Case "b = BO".