 06 Dec, 2016 2 commits


Ralf Jung authored

Robbert Krebbers authored

 05 Dec, 2016 1 commit


Robbert Krebbers authored
Using this new definition we can express being contractive using a Proper. This has the following advantages:  It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments).  A solve_contractive tactic can be implemented by extending the solve_proper tactic.

 29 Nov, 2016 1 commit


Robbert Krebbers authored

 24 Nov, 2016 1 commit


Robbert Krebbers authored

 23 Nov, 2016 4 commits


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

Robbert Krebbers authored

Robbert Krebbers authored

 22 Nov, 2016 6 commits


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.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 21 Nov, 2016 8 commits


Ralf Jung authored
In particular, make sure we always try eassumption before reflexivity.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 20 Nov, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 19 Nov, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
That range includes tabs and new lines. Thanks Morten for spotting this problem.

 17 Nov, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored
This way we can use set_solver to solve goals involving ∈.

Ralf Jung authored

Ralf Jung authored
This has bothered me repeatedly in proofs, now I finally got around to fix it at the source

Robbert Krebbers authored

 16 Nov, 2016 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 15 Nov, 2016 4 commits


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
(These instances are not defined for any FinMap to avoid overlapping instances for EqDecision, which may have awkward consequences for type class search).

 10 Nov, 2016 1 commit


Robbert Krebbers authored
Having Is_true as a type class caused problems with rewrite: when the rewrited lemma has a premise of the shape Is_true, the rewrite tactic will complain that it cannot find a type class instance, instead of generating a goal for that premise.
