Skip to content

Instantly share code, notes, and snippets.

Avatar

Juneyoung Lee aqjune

View GitHub Profile
@aqjune
aqjune / tactic.lean
Last active Mar 1, 2018
Creating random test from proposition using tactic library
View tactic.lean
open tactic
private constant mk_eq (sz:size) (x y:bitvector sz): x = y
constant smt_eq {sz:size}: sbitvec sz → sbitvec sz → Prop
theorem eq_add2 (sz:size): ∀ (x y: bitvector sz),
smt_eq (sbitvec.add (sbitvec.of_bv x) (sbitvec.of_bv y))
(sbitvec.of_bv (bitvector.add x y)) :=
by do
x ← intro `x,
@aqjune
aqjune / tactic2.lean
Created Mar 2, 2018
Just some copy and paste
View tactic2.lean
/-
constant eq_test {sz:size}: sbitvec sz → bitvector sz → Prop
axiom eq_const (sz:size): ∀ (z:ℤ),
eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)
meta instance eq_const_decidable (sz:size): decidable (∀ (z:ℤ),
eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)) :=
View example.lean
class C {α:ℕ → Type} :=
(myf:α 1 → α 1 → α 1)
(cx cy:α 1)
variable {α:ℕ → Type}
variable [s1:@C α]
include s1
def f1 := C.myf (C.cx α) (C.cy α)
def f2 := f1 /- don't know how to synthesize placeholder
View include.lean
class C {α:ℕ → Type} :=
(myf:α 1 → α 1 → α 1)
(cx cy:α 1)
variable {α':ℕ → Type}
variable [s1:@C α']
include α'
include s1
def f1 := C.myf (C.cx α') (C.cy α')
View foo.lean
inductive any
| val : ∀ (α:Type), α → any
def bar (n:nat):option nat :=
return n
def foo:option any :=
do
dummy ← bar 10,
return (any.val nat 3)
@aqjune
aqjune / move.cpp
Created Nov 20, 2018
C++'s move semantics - example
View move.cpp
#include <vector>
#include <iostream>
#include<utility>
using namespace std;
class C {
public:
int *ptr;
C(int val) {
cout << " Constructor: " << (intptr_t) this << endl;
View gist:6d2fcf86dc34265226198655362418d1
define <4 x i8*> @tinkywinky() {
%patatino = getelementptr i8, i8* undef, <4 x i64> undef
ret <4 x i8*> %patatino
}
=>
define <4 x i8*> @tinkywinky() {
ret <4 x i8*> undef
}
@aqjune
aqjune / fib.c
Last active Mar 26, 2020
Practice session 2 - fibonacci
View fib.c
unsigned fib(unsigned n) {
unsigned answ;
if (n <= 1)
answ = n;
else
answ = fib(n - 1) + fib(n - 2);
return answ;
}
View zero-null3.srctgt.ll
target datalayout="e"
;target datalayout="E" ; both is fine
define void @src(i8** %q) {
%ofs = shl i64 7, 60
%p = getelementptr i8, i8* null, i64 %ofs
store i8* %p, i8** %q
ret void
}