Use obtain in tactic mode in Lean theorem prover -

-

how use hypothesis of shape

h : exists x, p x

in tactic mode? in term mode use

obtain x hx, h,

it's same syntax:

example (a : type) (p : × a) : := begin   obtain x y, p, x end

you can of course re-enter tactic mode using begin...end after from.


Comments

Post a Comment

Popular posts from this blog

testing - Detect whether test has failed within fixture -

-
i debugging intermittent test failure. purposes want dump lot of debug information if test failed. dumping debug stuff quite slow process produces lot of data, not want every test. i using pytest , yield autouse fixture should work great @pytest.yield_fixture(scope="function", autouse=true) def dump_on_failue(request): prepare_debug_dump() yield if test_failed(request): debug_dump() the problem can't figure out how detect whether test has failed or not. there a questions already , note on pytest website : if request.node.rep_setup.failed: print ("setting test failed!", request.node.nodeid) elif request.node.rep_setup.passed: if request.node.rep_call.failed: print ("executing test failed", request.node.nodeid) unfortunately code not work anymore. there no rep_setup , rep_calls symbols in node object. tried dig request , node object, no luck. anybody knows how detect whether test ...
Read more

AbotX : How do you create a parallel crawler that stays on and can be added to at run time from new requests -

-
i have parallelcrawlerengine setup singleton , have alwaysonsitetocrawlprovider set singleton , passed parallelcrawlerengine. i can instantiate , leave nothing ok. can add site , crawl ok. if add site not crawl second site. i have looked @ example on site doesn't appear show how work , have new items added after initial execution. using .addsitestocrawl() adds them list seems stay in purgatory state of not being read. looking through logs 'site completed' message though site has not been recrawled [2016-07-11 11:17:18,361] [20 ] [info ] - crawl domain [http://www.existingsite.com/] completed in [0.0001118] seconds, crawled [361] pages and error if add new site [2016-07-11 11:17:33,365] [23 ] [error] - crawl domain [http://www.newsite.com/] failed after [0.0066498] seconds, crawled [361] pages [2016-07-11 11:17:33,365] [23 ] [error] - system.invalidoperationexception: cannot call dowork() after abortall() or dispose() have been called. @ abot.util.thre...
Read more

android - Create single AAR file from multiple modules using Gradle -

-
like many others, trying generate single aar file multi-modules android project. according this post , not supported android team because of various limitations (res & dependencies management, manifest merging, ...). i trying come own solution fits needs. know don't have duplicated resources , external dependencies (like support libraries) provided people using lib. my structure similar this: /root |- lib1 |- lib2 |- lib3 in order achieve goal, created 1 more library module, named distribute , include others modules. can share generated distribute.aar file. /root |- lib1 |- lib2 |- lib3 |- distribute this build.gradle file of distribute module: apply from: '../common.gradle' // configure properties shared accross modules apply plugin: 'com.android.library' def allmodules = rootproject.allprojects.collect { it.name } - [rootproject.name, name] def whitelabeldependencies = [ whitelabel1: allmodules - ['lib2'], whitel...
Read more