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 |