umedaikiti

type variable = X of int | Y of int
type assign = variable * bool
type literal = bool * variable
type clause = literal list
type cnf = clause list

type formula =
| And of formula * formula 
| Or of formula * formula
| Not of formula

umedaikiti

var buf = new ArrayBuffer(8);
var view = new Int32Array(buf);
view[0] = 0x44434241;
view[1] = 0x48474645;
var file = new File(["test", "あいうえお", buf], "test.txt", {type: "text/plain"});
document.getElementById("download").setAttribute("href", window.URL.createObjectURL(file));
document.getElementById("download").setAttribute("download", file.name);

umedaikiti

(*
TODO
- Improve readability and naming
- Complete proofs
*)

Inductive Action :=
| Out : nat -> Action
| In : nat -> Action
| Tau : Action.

umedaikiti

#[derive(PartialEq, Copy, Clone)]
enum State {
    Unknown,
    NotPrime,
    NotCarmichael
}

fn main() {
    let mut a = [State::Unknown; 1000000];
    a[0] = State::NotCarmichael;

umedaikiti

Require Import Omega.
Goal ~(exists f : nat -> nat, forall n : nat, f (f n) = n + 1).
Proof.
intro H.
destruct H as [f H].
assert (forall n : nat, f n = n + f 0).
intro n.
induction n.
reflexivity.
simpl.

umedaikiti

Section Binary.

Inductive Bits : nat -> Set :=
| xO : forall {m : nat}, Bits m -> Bits (S m)
| xI : forall {m : nat}, Bits m -> Bits (S m)
| xo : Bits 0
| xi : Bits 0.

Fixpoint to_nat {n : nat} (b : Bits n) : nat := match b with
| xi => 1

umedaikiti

Module FiniteRankedTree.
Inductive Forest {A : Set} {sigma : A -> nat} : nat -> Set :=
  | leaf : Forest O
  | sibl : RankedTree -> forall n, Forest n -> Forest (S n)
with
RankedTree {A : Set} {sigma : A -> nat} : Set := node : forall a, Forest (sigma a) -> RankedTree.
End FiniteRankedTree.

Module RankedTree.
Require Import List.

umedaikiti

with_slider_draw(k,makelist(i,i,1,7),
	proportional_axes = xy,
	xrange = [-3,3],
	yrange = [-3,3],
	xaxis=true,
	yaxis=true,
	grid = true,
	title = "animation" ,
	label([sconcat("k=",k-4),-1,2]),
	point_type=7,

umedaikiti

Section s1.

Axiom a : nat.
Variable b : nat.

Definition c : nat := 1.
Let d : nat := 1.

Print All.

umedaikiti

Require Import Arith.
(*
Check eq_nat_dec.

Definition update {A B : Set} (eq_dec : forall x y : A, {x = y} + {x <> y}) (f : A -> B) (x : A) (a : B) : A -> B :=
fun y => match eq_dec x y with
| left _ => a
| right _ => f y
end.
Check nat.