Tomer Libal shaolintl
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
| <div class="jumbotron"> | |
| <h1 class="display-4">Hello, world!</h1> | |
| <p class="lead">This is a simple hero unit, a simple jumbotron-style component for calling extra attention to featured content or information.</p> | |
| <hr class="my-4"> | |
| <p>It uses utility classes for typography and spacing to space content out within the larger container.</p> | |
| <p class="lead"> | |
| <a class="btn btn-primary btn-lg" href="#" role="button">Learn more</a> | |
| </p> | |
| </div> |
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
| df = pd.read_csv('https://d17h27t6h515a5.cloudfront.net/topher/2016/December/584be5d4_titanic-data/titanic-data.csv') |
shaolintl
/ Bloat4.smt
Last active
April 18, 2017 16:13
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
| ; Starting query at ./Bloat4.fst(3,0-3,38) | |
| (declare-fun label_1 () Bool) | |
| (push) | |
| ; <fuel='2' ifuel='1'> | |
| (assert (! (= MaxFuel | |
| (SFuel (SFuel ZFuel))) | |
| :named @MaxFuel_assumption)) | |
| (assert (! (= MaxIFuel | |
| (SFuel ZFuel)) |
shaolintl
/ Bloat1.smt
Created
April 18, 2017 15:48
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
| ; Starting query at ./Bloat1.fst(3,0-3,32) | |
| (declare-fun label_1 () Bool) | |
| (push) | |
| ; <fuel='2' ifuel='1'> | |
| (assert (! (= MaxFuel | |
| (SFuel (SFuel ZFuel))) | |
| :named @MaxFuel_assumption)) | |
| (assert (! (= MaxIFuel | |
| (SFuel ZFuel)) |
shaolintl
/ Bloat2.smt
Created
April 18, 2017 15:46
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
| ; Starting query at ./Bloat2.fst(3,0-5,12) | |
| (declare-fun label_2 () Bool) | |
| (declare-fun label_1 () Bool) | |
| ;;;;;;;;;;;;;;;;Uvar typing | |
| (assert (! (HasType (Tm_uvar 26534) | |
| Tm_type) | |
| :named uvar_typing_26534)) | |
| ;;;;;;;;;;;;;;;;Uvar typing | |
| (assert (! (HasType (Tm_uvar 26534) | |
| Tm_type) |
shaolintl
/ Bloat3.smt
Last active
April 18, 2017 15:43
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
| ; Starting query at ./Bloat3.fst(4,0-6,12) | |
| (declare-fun label_2 () Bool) | |
| (declare-fun label_1 () Bool) | |
| (push) | |
| ; <fuel='2' ifuel='1'> | |
| (assert (! (= MaxFuel | |
| (SFuel (SFuel ZFuel))) | |
| :named @MaxFuel_assumption)) | |
| (assert (! (= MaxIFuel |
shaolintl
/ gist:8d066532d66c6a1900f46b8a096e1389
Created
March 27, 2017 13:01
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
| letrecs: | |
| (FStar_Syntax_Syntax.bv * FStar_Syntax_Syntax.arg_qualifier Prims.option) | |
| list = [] |
shaolintl
/ gist:8955d9a27ba5608a0e184c2d7e041a43
Created
March 27, 2017 13:01
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
| bs: (FStar_Syntax_Syntax.bv * FStar_Syntax_Syntax.aqual) list = | |
| [({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "n"; | |
| idRange = | |
| {FStar_Range.def_range = 576462967432871938L; | |
| use_range = 576462967432871938L}}; | |
| index = <abstr>; | |
| sort = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_delayed |
shaolintl
/ gist:ade819bf7b82e5050a8d34f26b2b94e1
Created
March 27, 2017 13:00
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
| g: FStar_TypeChecker_Env.guard_t = | |
| {FStar_TypeChecker_Env.guard_f = FStar_TypeChecker_Common.Trivial; | |
| deferred = []; univ_ineqs = ([], []); implicits = []} |
shaolintl
/ gist:d7033ae62763c4930074721a046f7802
Created
March 27, 2017 12:59
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
| body: FStar_Syntax_Syntax.term = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_delayed | |
| (FStar_Util.Inl | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_match | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_delayed | |
| (FStar_Util.Inl | |
| ({FStar_Syntax_Syntax.n = |
NewerOlder