Instantly share code, notes, and snippets.

Juneyoung Lee aqjune

Last active Mar 1, 2018
Creating random test from proposition using tactic library
View tactic.lean
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
 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,
Created Mar 2, 2018
Just some copy and paste
View tactic2.lean
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
 /- 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)) :=
Created Mar 15, 2018
Lean example
View example.lean
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
 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
Created Mar 16, 2018
Lean code
View include.lean
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
 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 α')
Created Mar 19, 2018
View foo.lean
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
 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)
Created Nov 20, 2018
C++'s move semantics - example
View move.cpp
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
 #include #include #include using namespace std; class C { public: int *ptr; C(int val) { cout << " Constructor: " << (intptr_t) this << endl;
Last active Oct 8, 2022
Useful clang/opt options
View llvmclangcmds.md

Parameters to clang

``````-fno-discard-value-names
-g0
Don’t generate any debug info (default).
-gline-tables-only
``````
Created Jan 13, 2020
undefptr-example
View gist:6d2fcf86dc34265226198655362418d1
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
 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 }
Last active Mar 26, 2020
Practice session 2 - fibonacci
View fib.c
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
 unsigned fib(unsigned n) { unsigned answ; if (n <= 1) answ = n; else answ = fib(n - 1) + fib(n - 2); return answ; }
Created May 18, 2020
View zero-null3.srctgt.ll
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
 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 }