Skip to content

Instantly share code, notes, and snippets.

View KeenS's full-sized avatar

κeen KeenS

457 followers · 55 following
View GitHub Profile
@KeenS
KeenS / 2-8.v
Created April 13, 2014 16:14
Require Import Arith.
Goal forall m n : nat, (n * 10) + m = (10 * n) + m.
Proof.
intros.
rewrite mult_comm.
reflexivity.
Qed.
@KeenS
KeenS / 2-9.v
Created April 13, 2014 16:38
Require Import Arith.
Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
intros.
rewrite (plus_assoc (n + m) p q).
rewrite (plus_assoc (n + p) m q).
rewrite <- (plus_assoc n m p).
rewrite <- (plus_assoc n p m).
rewrite (plus_comm m p).
@KeenS
KeenS / 2-9.v
Created April 13, 2014 17:03
Require Import Arith.
Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
intros.
rewrite (plus_assoc (n + m) p q).
rewrite (plus_assoc (n + p) m q).
rewrite <- (plus_assoc n m p).
rewrite <- (plus_assoc n p m).
rewrite (plus_comm m p).
@KeenS
KeenS / 2-10.v
Created April 13, 2014 17:27
Parameter G : Set.
Parameter mult : G -> G -> G.
Notation "x * y" := (mult x y).
Parameter one : G.
Notation "1" := one.
Parameter inv : G -> G.
Notation "/ x" := (inv x).
Axiom mult_assoc : forall x y z, x * (y * z) = (x * y) * z.
Axiom one_unit_l : forall x, 1 * x = x.
@KeenS
KeenS / 3-11.v
Created April 26, 2014 16:32
Require Import Arith.
Fixpoint sum_odd(n:nat) : nat :=
match n with
| 0 => 0
| S m => 1 + m + m + sum_odd m
end.
Goal forall n, sum_odd n = n * n.
Proof.
@KeenS
KeenS / gist:4b889e04f2d82f259885
Created July 22, 2014 15:13
|
|
. ..
\ . .. /
\. .. ../
|| . .|
|| .. |
|| . .. |
. ..
. ..
@KeenS
KeenS / mirah log
Created July 23, 2014 06:39
スクリプトは 2014年07月23日 15時16分18秒
に開始しました%
(:branch master :cwd ~/compile/mirah)[?1h=rrm -rf dist/[?1l>
%
(:branch master :cwd ~/compile/mirah)[?1h=mmvn[?1l>
@KeenS
KeenS / compile_error.diff
Created July 23, 2014 15:33
diff --git a/src/org/mirah/tool/mirahc.mirah b/src/org/mirah/tool/mirahc.mirah
index 754008f..dcbe23e 100644
--- a/src/org/mirah/tool/mirahc.mirah
+++ b/src/org/mirah/tool/mirahc.mirah
@@ -31,12 +31,13 @@ class Mirahc < MirahTool
end
def self.main(args:String[]):void
- result = compile(args)
+ mirahc = Mirahc.new()
@KeenS
KeenS / mirah-parser.diff
Created July 24, 2014 16:37
diff --git a/src/mirahparser/impl/Mirah.mmeta b/src/mirahparser/impl/Mirah.mmeta
index 520b75b..b4c3d36 100644
--- a/src/mirahparser/impl/Mirah.mmeta
+++ b/src/mirahparser/impl/Mirah.mmeta
@@ -1293,7 +1293,8 @@ parser EscapeParser {
|codepoint
);
- regex: unicode_escape
+ regex: "\\\\" ! {"\\\\"}
@KeenS
KeenS / mirah-parser.error
Last active August 29, 2015 14:04
java -jar /home/kim/compile/mirah-parser/javalib/mirahc.jar --classpath /home/kim/compile/mirah-parser/javalib/mirah.jar -d /home/kim/compile/mirah-parser/build ./src/org/mirah/ast/meta.mirah
./src/org/mirah/ast/meta.mirah:18:
ERROR: Cannot find class org.mirahparser.ast.mirah.lang.ast.Block
import mirah.lang.ast.Block
^^^^^^^^^^^^^^^^^^^^^^^^^^^
./src/org/mirah/ast/meta.mirah:19:
ERROR: Cannot find class org.mirahparser.ast.mirah.lang.ast.CallSite
import mirah.lang.ast.CallSite