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