This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
TODO | |
- Improve readability and naming | |
- Complete proofs | |
*) | |
Inductive Action := | |
| Out : nat -> Action | |
| In : nat -> Action | |
| Tau : Action. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#[derive(PartialEq, Copy, Clone)] | |
enum State { | |
Unknown, | |
NotPrime, | |
NotCarmichael | |
} | |
fn main() { | |
let mut a = [State::Unknown; 1000000]; | |
a[0] = State::NotCarmichael; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Section s1. | |
Axiom a : nat. | |
Variable b : nat. | |
Definition c : nat := 1. | |
Let d : nat := 1. | |
Print All. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
NewerOlder