Tomer Libal shaolintl
shaolintl
/ gist:5372d3f3ea57ee7f3d3ee5da88dc29e3
Created
March 21, 2017 14: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
| simple.fst(3,31-3,34) (Tm_arrow) | |
| Checking binders x#623:(x#6:int{(b2t (op_GreaterThanOrEqual x@0 0))}) at type Type | |
| simple.fst(3,12-3,23) (Tm_delayed-resolved) | |
| Checking binders x#624:int at type Type | |
| simple.fst(3,14-3,17) (Tm_fvar: int) | |
| Computed return type Type; expected type Type | |
| check_and_ascribe: type is Type<:Type guard is {}, {} | |
| Return comp type is Tot Type | |
| Pushing binder x#624 at type int | |
| simple.fst(3,12-3,23)) Checking refinement formula (b2t (op_GreaterThanOrEqual x 0)); binder is x#624 |
shaolintl
/ let-e-val.debug
Created
March 21, 2017 13:31
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
| e: FStar_Syntax_Syntax.term = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_abs | |
| ([({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "n"; | |
| idRange = | |
| {FStar_Range.def_range = 576462967432871938L; | |
| use_range = 576462967432871938L}}; | |
| index = <abstr>; | |
| sort = |
shaolintl
/ let-lbdef.debug
Created
March 20, 2017 13:51
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
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_abs | |
| ([({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
/ let-lbtyp.debug
Created
March 20, 2017 13:51
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
| {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 = | |
| {FStar_Syntax_Syntax.n = |
shaolintl
/ check_top_level_lbs.debug
Created
March 20, 2017 13: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
| lbs: FStar_Syntax_Syntax.letbinding Prims.list = | |
| [{FStar_Syntax_Syntax.lbname = | |
| FStar_Util.Inr | |
| {FStar_Syntax_Syntax.fv_name = | |
| {FStar_Syntax_Syntax.v = | |
| {FStar_Ident.ns = | |
| [{FStar_Ident.idText = "Simple"; | |
| idRange = | |
| {FStar_Range.def_range = 468374918518554626L; | |
| use_range = 468374918518554626L}}]; |
shaolintl
/ let-e-e.debug
Created
March 17, 2017 17:37
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
| e: FStar_Syntax_Syntax.term = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_abs | |
| ([({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "n"; | |
| idRange = | |
| {FStar_Range.def_range = 576462967432871938L; | |
| use_range = 576462967432871938L}}; | |
| index = <abstr>; | |
| sort = |
shaolintl
/ let-e-t.debug
Created
March 17, 2017 17:34
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.typ = | |
| {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
/ let-e-lb.debug
Created
March 17, 2017 17: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
| lb: FStar_Syntax_Syntax.letbinding = | |
| {FStar_Syntax_Syntax.lbname = | |
| FStar_Util.Inr | |
| {FStar_Syntax_Syntax.fv_name = | |
| {FStar_Syntax_Syntax.v = | |
| {FStar_Ident.ns = | |
| [{FStar_Ident.idText = "Simple"; | |
| idRange = | |
| {FStar_Range.def_range = 468374918518554626L; | |
| use_range = 468374918518554626L}}]; |
shaolintl
/ let-t-to-type.debug
Created
March 17, 2017 17:10
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
/ let-e-lbdef.debug
Created
March 17, 2017 16:55
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
| e: FStar_Syntax_Syntax.term = | |
| {FStar_Syntax_Syntax.n = | |
| FStar_Syntax_Syntax.Tm_abs | |
| ([({FStar_Syntax_Syntax.ppname = | |
| {FStar_Ident.idText = "n"; | |
| idRange = | |
| {FStar_Range.def_range = 576462967432871938L; | |
| use_range = 576462967432871938L}}; | |
| index = <abstr>; | |
| sort = |