I hereby claim:
- I am mzp on github.
- I am mzp (https://keybase.io/mzp) on keybase.
- I have a public key ASAwwDPqzgm4PlvU_jfr-ryuG8e2dvbb74lIj3jnHgC4mwo
To claim this, I am signing this object:
*.scpt filter=osa |
I hereby claim:
To claim this, I am signing this object:
FROM buildpack-deps:stretch | |
# skip installing gem documentation | |
RUN mkdir -p /usr/local/etc \ | |
&& { \ | |
echo 'install: --no-document'; \ | |
echo 'update: --no-document'; \ | |
} >> /usr/local/etc/gemrc | |
ENV RUBY_MAJOR 2.5 |
see: https://github.com/bleis-tift/SmlSharpContrib
SML#のライブラリが足りないのでなんとかしたい。
(* compile with Coq 8.4pl2 *) | |
Fixpoint evenb (n:nat) : bool := | |
match n with | |
| O => true | |
| S O => false | |
| S (S n') => evenb n' | |
end. | |
Definition negb (b:bool) : bool := | |
match b with |
Inductive Term : Set := | |
| T | |
| F | |
| TIf (_ : Term) (_ : Term) (_ : Term). | |
Inductive Step : Term -> Term -> Prop := | |
| EIfTrue : forall (t1 t2 : Term), Step (TIf T t1 t2) t1 | |
| EIfFalse : forall (t1 t2 : Term), Step (TIf F t1 t2) t2 | |
| EIf : forall (t1 t1' t2 t3 : Term), Step t1 t1' -> Step (TIf t1 t2 t3) (TIf t1' t2 t3). |
_require "basis.smi" |
Xen Minimal OS! | |
start_info: 000000000018b000(VA) | |
nr_pages: 0x10000 | |
shared_inf: 0x1de99000(MA) | |
pt_base: 000000000018e000(VA) | |
nr_pt_frames: 0x5 | |
mfn_list: 000000000010b000(VA) | |
mod_start: 0x0(VA) | |
mod_len: 0 | |
flags: 0x0 |