@jonsterling That's quite new. I have so many half baked special purpose ad-hoc versions of it that it's nice to have a generic tactic...
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@edwinbrady If I'm understanding that correctly testRecTy is the type of testRec and it's figured out by the "proof search" call? -
@seanparsons Yes. "search" is a tactic, and "proof" starts a proof script. - 4 more replies
New conversation -
-
-
@edwinbrady Types as labels feels a bit iffy: no way to write a function that generates `FieldType l r a` values by search at runtime? -
@bentnib There would be, but compile time search seems better if possible. Anything could be a label - I'll try to make it polymorphic.
End of conversation
New conversation -
-
-
@edwinbrady I noticed "with HList" doesn't seem necessary w/ HLists. Like, it's unambiguous once you get a few elems of different types? -
@pdxleif Yes, the others will just not typecheck so only HList is left.
End of conversation
New conversation -
-
-
@edwinbrady hmm, add offsets and it could represent a C struct. -
@kryptiskt Interesting thought, as a component of an EDSL perhaps. - 1 more reply
New conversation -
-
-
@jonsterling@edwinbrady ... But it's probably very wrong to think that way? -
@aloiscochard@jonsterling It's a limited form of type inference. Probably best avoided in general, but handy here. - 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.