This file contains hidden or 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 Coq.Unicode.Utf8 Arith FunctionalExtensionality String Coq.Program.Equality. | |
Set Implicit Arguments. | |
Ltac invert H := inversion H; clear H; subst. | |
Ltac invert1 H := invert H; []. | |
Inductive star A (R : A -> A -> Prop) : A -> A -> Prop := | |
| StarRefl : forall x, | |
star R x x |
This file contains hidden or 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 'fileutils' | |
Dir.glob('*_assignsubmission_file_*').each do |filename| | |
if m = /(.+)_\d+_assignsubmission_file_(.+)/.match(filename) | |
_, username, orig_filename = *m | |
FileUtils.mkdir_p(username) # if it exists, do nothing | |
FileUtils.mv(filename, username + '/' + orig_filename) | |
end | |
end |
This file contains hidden or 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
// inspired: http://journal.stuffwithstuff.com/2013/04/23/playing-with-generics-in-typescript-0.9.0/ | |
class Base { | |
foo() : void {} | |
} | |
// If `Derived' has no addional method, we'll get different results | |
class Derived extends Base { | |
bar() : void {} | |
} |
This file contains hidden or 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
// X. Yan, J. Guo, Y. Lan, and X. Cheng, A Biterm Topic Model for Short Texts, | |
// in WWW. ACM, 2013, pp. 1445–145 | |
import scala.collection._ | |
import scala.io.Source | |
import scala.util.Random | |
import java.io._ | |
class BTM(val alpha:Double, val beta:Double, val k:Int, val iterN:Int) { | |
private var words:Array[String] = null |
This file contains hidden or 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
Definition id {A} : A -> A := fun x => x. | |
Arguments id {A} / x. | |
Definition compose {A B C} : (B -> C) -> (A -> B) -> (A -> C) | |
:= fun g f x => g (f x). | |
Notation "g 'o' f" := (compose g f) (left associativity, at level 37). | |
Arguments compose {A B C} f g x /. |
This file contains hidden or 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
(test (match {4 2 1 9} (List Integer) | |
{[(foldr (lambda [$i $l] | |
<cons $a_i l>) | |
<nil> | |
(between 1 4)) | |
[a_1 a_2 a_3 a_4]]})) |
This file contains hidden or 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
#!/usr/bin/env ruby | |
require 'thor' | |
require 'mechanize' | |
USER = '' | |
PASS = '' | |
class Report < Thor | |
desc 'submit src1 src2 ...', 'Submit code' |
This file contains hidden or 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
#sideNavi, | |
.leafThemeTitle, | |
.leafThemeTitleMap, | |
.themeTopic { | |
display: none !important; | |
} | |
.topTitleBar, | |
#kijiBox, | |
.kijiTitle, |
This file contains hidden or 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
#!/usr/bin/env ruby | |
require 'optparse' | |
require 'pathname' | |
require 'tmpdir' | |
libraries = %w|/Applications/Processing.app/Contents/Resources/Java/core.jar| | |
compiler = 'scalac' | |
OptionParser.new {|opt| | |
opt.on('-w', '--watch') { compiler = 'fsc' } |
This file contains hidden or 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 'open-uri' | |
require 'RMagick' | |
if ARGV.length != 2 | |
puts 'Usage: ./ame.rb latitude longtitude' | |
exit | |
end | |
url = 'http://tokyo-ame.jwa.or.jp/mesh/100/%s.gif' % | |
Time.at((Time.now - 30).to_i / 300 * 300).strftime('%Y%m%d%H%M') |
NewerOlder