coq - Applying hypotesis to a variable -

-

let's i'm in middle of proof , have hypotheses these:

a : nat b : nat c : nat h : somepred b

and definition of somepred says:

definition somepred (p:nat) (q:nat) : prop := forall (x : nat), p(x, p, q).

how apply h c , p(c, a, b)?

the answer is:

specialize h c.

Comments

Post a Comment

Popular posts from this blog

angularjs - Showing an empty as first option in select tag -

-
my app showing empty select field first entry. have read other solution given , tried still not working. my controller code is: .controller('usercreatecontroller', function(user,profile,auth) { alert("hello"); var vm = this; vm.type = 'create'; profile.all() //this service fetch profiles shown in select field .success(function(data){ vm.profile = data; }); vm.userdata.profile = vm.profile[0]; //here have set default value select field and html page is: <label class="col-sm-2 control-label">profile</label> <div class="col-sm-8"> <select ng-model="user.userdata.profile" ng-options="person._id person.profilename person in user.profile"> </select> </div> hierarchy of vm.profile { "_id": 46, "profile": objectid("5516498e95b84548156db754"), "isactive": true, "password": "$2...
Read more

qt - Change color of QGraphicsView rubber band -

-
i know it's possible change color of rubber band rectangle way: qrubberband rubberband = new qrubberband(qrubberband::rectangle, this); qpalette pal; pal.setbrush(qpalette::highlight, qbrush(qt::white)); rubberband->setpalette(pal); but here way achieve rubber band, rendered qgraphicsview when rubberbanddrag mode active? or in "global scope"? i'm sorry wrote question, i've looked solution long time, , nothing. few minutes after asking, found solution setting stylesheet. i'm sharing it. just go designer of qt creator, click on canvas (qgraphicsview). in "qwidget" part find "stylesheet", edit it, , put like: selection-background-color: rgba(255, 255, 255, 128); that's :-). thanks.
Read more

c++ - Print Preview in Qt -

-
i want preview page or want have print preview. preview window opening contents of qt window not comming in it. code print preview follows: void user::on_actionprintpreview_triggered() { qprinter printer(qprinter::highresolution); qprintpreviewdialog preview(&printer, this); connect(&preview, signal(paintrequested(qprinter *)), this, slot(print(qprinter *))); preview.exec(); } void user::print(qprinter *printer) { // print page qpainter painter(printer); int w = printer->pagerect().width(); int h = printer->pagerect().height(); qrect page(0, 0, w, h); qfont font = painter.font(); font.setpixelsize((w+h)/100); painter.setfont(font); painter.drawtext(page, qt::alignbottom | qt::alignright, qdatetime::currentdatetime(). tostring(qt::defaultlocaleshortdate)); page.adjust(w/20, h/20, -w/20, -h/20); } how can content of qt window in it. doing wrong. please m...
Read more