 25 Nov, 2016 9 commits


Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

JacquesHenri Jourdan authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
No longer `put box_own_prop γ P` in the invariant, it is persistent.

JacquesHenri Jourdan authored

 24 Nov, 2016 12 commits


JacquesHenri Jourdan authored


JacquesHenri Jourdan authored


Ralf Jung authored

JacquesHenri Jourdan authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

JacquesHenri Jourdan authored
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

Robbert authored
ProofMode intro patterns: accept _ as part of variable names @robbertkrebbers beat this. ;) See merge request !29

Ralf Jung authored

 23 Nov, 2016 12 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored
Use notation N @⊆ E to avoid ambiguity. Since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be illtyped. See merge request !24

Ralf Jung authored
Fractional typeclass. A typeclass for fractional assertions, that is assertions that depend on a fraction and that can be split. This is used to derive generically a few other instances for framing , destructing, combining and spliting assertions of sums of fractions. I found it usefull when doing fractionheavy proofs in LambdaRust. The Right Way To Do It would be to use a typeclass over the *predicate* itself. Unfortunately, the unification algorithm of typeclasses is not powerful enough to do the right betaexpansion that would expose the predicate applied to some fraction. Instead, the `Fractional` type class has as parameters both the predicate and the applied form that can be directly unified with the fractured assertion. Not very pretty. I wonder whether I should split this into two type classes: the first one would depend only on the predicate and would actually state the fractionality of it, and the second would do the betaexpansion job. What do you think? See merge request !23

JacquesHenri Jourdan authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 22 Nov, 2016 7 commits


Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
We do this by introducing a type class UpClose with notation ↑. The reason for this change is as follows: since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be illtyped.


Ralf Jung authored

Robbert Krebbers authored
