|
|
|
@1695
|
9 years |
mulligan |
Progress on CostsProof?.ma file.
|
|
|
|
@1693
|
9 years |
mulligan |
Changes to ASMCosts and CostsProofs? files to get everything working again.
|
|
|
|
@1692
|
9 years |
mulligan |
resolved conflict in asm costs this morning
|
|
|
|
@1658
|
9 years |
mulligan |
asm costs changes from today
|
|
|
|
@1650
|
9 years |
mulligan |
changes over the last couple of days: stuck due to matita producing …
|
|
|
|
@1648
|
9 years |
mulligan |
new version of utilities/monad.ma with typecheck command comented out
|
|
|
|
@1620
|
9 years |
sacerdot |
One of the mutual cases of the open proof is practically finished.
|
|
|
|
@1619
|
9 years |
sacerdot |
Major advancement.
|
|
|
|
@1587
|
9 years |
mulligan |
changes from today, including removing indexing of problematic …
|
|
|
|
@1581
|
9 years |
mulligan |
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
|
|
|
|
@1579
|
9 years |
mulligan |
Finished proof with simpler statement, making everything a lot nicer
|
|
|
|
@1577
|
9 years |
mulligan |
A lot more cases added to the proof at the bottom of …
|
|
|
|
@1576
|
9 years |
mulligan |
big changes to proofs, just two small cases remain and a few …
|
|
|
|
@1575
|
9 years |
mulligan |
Changes to specifications on execute functions
|
|
|
|
@1573
|
9 years |
mulligan |
more complicated than it appears :(
|
|
|
|
@1571
|
9 years |
mulligan |
small changes
|
|
|
|
@1570
|
9 years |
sacerdot |
Dependent type crazyness.
|
|
|
|
@1567
|
9 years |
mulligan |
more work on big proof, 2.5 cases left
|
|
|
|
@1564
|
9 years |
sacerdot |
Commit where we use a dependently typed version of bigops.
I am now …
|
|
|
|
@1561
|
9 years |
sacerdot |
More dependent types to accomodate the statement.
|
|
|
|
@1558
|
9 years |
sacerdot |
Snapshot before moving things to ASMCosts.ma.
|
|
|
|
@1556
|
9 years |
mulligan |
submitting to avoid conflicts
|
|
|
|
@1554
|
9 years |
sacerdot |
Major progress in the proof.
|
|
|
|
@1549
|
9 years |
mulligan |
removed cruft from costsproof.ma file so claudio can work in parallel
|
|
|
|
@1548
|
9 years |
sacerdot |
…
|
|
|
|
@1544
|
9 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
|
@1534
|
9 years |
mulligan |
committing my changes to interpret to prevent any further conflicts
|
|
|
|
@1522
|
9 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
|
@1514
|
9 years |
mulligan |
changes from today. matita keeps dieing
|
|
|
|
@1511
|
9 years |
mulligan |
proofs, added, changes to execute_1_0 function therefore required to …
|
|
|
|
@1509
|
9 years |
mulligan |
i hate subtraction over the nats
|
|
|
|
@1506
|
9 years |
mulligan |
changes to costs proof over weekend
|
|
|
|
@1503
|
9 years |
mulligan |
inductive type complete
|
|
|
|
@1502
|
9 years |
mulligan |
changes to inductive defn
|
|
|
|
@1501
|
9 years |
sacerdot |
We must take in account the labelled_p predicate.
|
|
|
|
@1500
|
9 years |
sacerdot |
Proof sketch for one of the two main proofs.
|
|
|
|
@1499
|
9 years |
mulligan |
part way through main statement transcription
|
|
|
|
@1498
|
9 years |
mulligan |
added new file for proof that costs are preserved at asm level
|
