I hereby claim:
- I am rindphi on github.
- I am dscheurer (https://keybase.io/dscheurer) on keybase.
- I have a public key ASDbCaKb2RPNzwWoQM2nVMThGjDdvA_Wm9nSJ_PCyyJMmgo
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
#!/usr/bin/fish | |
set fish_greeting | |
function res_x_prompt | |
echo -n 'Please enter the horizontal resolution [1024]: ' | |
end | |
function res_y_prompt | |
echo -n 'Please enter the vertical resolution [768]: ' | |
end |
package example; | |
import java.io.File; | |
import java.util.HashMap; | |
import java.util.List; | |
import org.key_project.util.collection.ImmutableSLList; | |
import org.key_project.util.java.StringUtil; | |
import de.uka.ilkd.key.control.*; |
/*@ public normal_behavior | |
@ ensures (a != 0 || b != 0) ==> | |
@ (a % \result == 0 && b % \result == 0 && | |
@ (\forall int x; x > 0 && a % x == 0 && b % x == 0; | |
@ \result % x == 0)); | |
@*/ | |
public static int gcd(int a, int b) { | |
if (a < 0) a = -a; | |
if (b < 0) b = -b; |
/*@ public normal_behavior | |
@ ensures (a != 0 || b != 0) ==> | |
@ (a % \result == 0 && b % \result == 0 && | |
@ (\forall int x; x > 0 && a % x == 0 && b % x == 0; | |
@ \result % x == 0)); | |
@*/ | |
public static int gcd(int a, int b) { | |
if (a < 0) a = -a; | |
//@ merge_point |
public class Find { | |
//@ ghost int f_iLastRun; | |
// Everything covered | |
/*@ public normal_behavior | |
@ ensures | |
@ ((\exists int i; i >= 0 && i < arr.length; arr[i] == n) ==> | |
@ (arr[\result] == n && \result == f_iLastRun) | |
@ ) | |
@ && ((\forall int i; i >= 0 && i < arr.length; arr[i] != n) ==> \result == -1) |
package example; | |
import java.io.File; | |
import java.util.HashMap; | |
import java.util.LinkedList; | |
import java.util.List; | |
import java.util.Set; | |
import org.key_project.util.collection.ImmutableSet; |
(* | |
Compile to PDF with | |
coqc firstorder.v ; coqdoc --latex --no-lib-name -s -p "\usepackage{parskip}\renewcommand{\thesection}{\arabic{section}}" firstorder.v ; pdflatex firstorder.tex | |
*) | |
Require Import Coq.Strings.String. | |
Require Import Coq.Vectors.VectorDef. | |
Require Import Coq.Relations.Relation_Definitions. | |
Module firstorder. |
#!/usr/bin/python3 | |
import xml.etree.ElementTree as ET | |
import re | |
import sys | |
import os | |
import pyperclip | |
from pathlib import Path | |
from subprocess import call | |
########################################################################### |
#!/usr/bin/python3 | |
import xml.etree.ElementTree as ET | |
import re | |
import sys | |
import os | |
import threading | |
from pathlib import Path | |
from subprocess import call | |
########################################################################### |