Tomer Libal shaolintl
shaolintl
/ gist:761bce2bff1b869ec079f5c3e890fc97
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
| c: (FStar_Syntax_Syntax.comp', Prims.unit) FStar_Syntax_Syntax.syntax = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Total | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_fvar | |
| {FStar_Syntax_Syntax.fv_name = | |
| {FStar_Syntax_Syntax.v = | |
| {FStar_Ident.ns = | |
| [{FStar_Ident.idText = "Prims"; | |
| idRange = |
shaolintl
/ gist:c877381b86f143e402065e652d3a0122
Created
March 27, 2017 12:58
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
| t: FStar_Syntax_Syntax.term = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_arrow | |
| ([({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "x"; | |
| idRange = | |
| {FStar_Range.def_range = 468376023398924290L; | |
| use_range = 468376023398924290L}}; | |
| index = <abstr>; | |
| sort = |
shaolintl
/ gist:db852beefddba91b5db1cf54b6f13e4c
Created
March 22, 2017 16:27
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
| hd: FStar_Syntax_Syntax.bv = | |
| {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:591b47957a63cd797999f411c731bba3
Created
March 22, 2017 16:12
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
| expected_t: | |
| (FStar_Syntax_Syntax.term', FStar_Syntax_Syntax.term') | |
| FStar_Syntax_Syntax.syntax = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_delayed | |
| (FStar_Util.Inl | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_refine | |
| ({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "x"; |
shaolintl
/ gist:f7f7083687bc403d0d08bb6e1ee07638
Created
March 22, 2017 15:22
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.arg_qualifier option) 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_unknown; |
shaolintl
/ gist:32c1a2790b7a9ef46f2eb4349ab4ccf2
Created
March 22, 2017 11:20
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
| c_expected: | |
| (FStar_Syntax_Syntax.comp', Prims.unit) FStar_Syntax_Syntax.syntax = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Total | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_fvar | |
| {FStar_Syntax_Syntax.fv_name = | |
| {FStar_Syntax_Syntax.v = <abstr>; | |
| ty = | |
| {FStar_Syntax_Syntax.n = |
shaolintl
/ gist:4bf6eaa2597d2b8c9fe0e903a84ab852
Created
March 22, 2017 11:19
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_expected: (FStar_Syntax_Syntax.bv * FStar_Syntax_Syntax.aqual) Prims.list | |
| = | |
| [({FStar_Syntax_Syntax.ppname = <abstr>; index = <abstr>; | |
| sort = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_delayed | |
| (FStar_Util.Inl | |
| ({FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_refine | |
| ({FStar_Syntax_Syntax.ppname = <abstr>; index = <abstr>; |
shaolintl
/ gist:e3d1940d403e986eea92065a4e2bbd8f
Created
March 21, 2017 16:16
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:(x#6:int{(b2t (op_GreaterThanOrEqual x@0 0))}) -> Tot int) |
shaolintl
/ abs-body.debug
Created
March 21, 2017 14:33
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 = |
shaolintl
/ abs-binders.debug
Created
March 21, 2017 14:32
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.binders = | |
| [({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_unknown; | |
| tk = {contents = None}; |