Commits · 024ad110602842e9722e0710351c841a1791ce5e · Rice Wine / Iris

11 Jan, 2018 2 commits
- Introduce monPred_ex, add monPred_in rules (attemp at removing abstract views from iGPS. · 024ad110
  Jacques-Henri Jourdan authored Jan 11, 2018
  
  024ad110
- Better follow naming convention: biIndex. · b4a7ba86
  Jacques-Henri Jourdan authored Jan 10, 2018
  
  b4a7ba86
10 Jan, 2018 1 commit
- Renaming monPred_car -> monPred_at · 8bd95fb9
  Jacques-Henri Jourdan authored Jan 10, 2018
  
  8bd95fb9
29 Dec, 2017 2 commits
- Merge branch 'janno/monfun' into 'gen_proofmode' · 817b8294
  Jacques-Henri Jourdan authored Dec 29, 2017
```
Construct BI on monotone function spaces.

See merge request FP/iris-coq!92
```
  817b8294
- Merge branch 'jh/bi_morphism' into 'janno/monfun' · 9a06dcc6
  Jacques-Henri Jourdan authored Dec 29, 2017
```
Proof mode support for monotonous predicates.

See merge request FP/iris-coq!100
```
  9a06dcc6
23 Dec, 2017 2 commits
- New instances for monpred_car and bi_plainly. · c8814e31
  Jacques-Henri Jourdan authored Dec 23, 2017
  
  c8814e31
- Trying to improve IntoWand for monPred_car: whenever it's possible, we try to... · 36c9602c
  Jacques-Henri Jourdan authored Dec 23, 2017
```
Trying to improve IntoWand for monPred_car: whenever it's possible, we try to change the view automatically.
```
  36c9602c
22 Dec, 2017 33 commits
- Fix Hint Mode. · d927b406
  Jacques-Henri Jourdan authored Dec 19, 2017
  
  d927b406
- Monpred : try to fix intowand instances. · 7c714af0
  Jacques-Henri Jourdan authored Dec 19, 2017
  
  7c714af0
- Add some tests. · d52fc276
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  d52fc276
- Weaken monPred_bi_embedding. A bi index is always inhabited. · a1f630a6
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  a1f630a6
- Tweak. · 128c9125
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  128c9125
- Name some variables. · 46ffdc4a
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  46ffdc4a
- Documentation. · 2352d3a9
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  2352d3a9
- Add hint mode. Add Implicit types. · 99929dca
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  99929dca
- New typeclass AsValid', used when the BI is known in advance. · 96d145ad
  Jacques-Henri Jourdan authored Dec 17, 2017
  
  96d145ad
- MonoidHommomorphism instances for embeddings. · ef06857c
  Jacques-Henri Jourdan authored Dec 17, 2017
  
  ef06857c
- Improve proofmode for monpred. · bd3a8a9f
  Jacques-Henri Jourdan authored Dec 15, 2017
  
  bd3a8a9f
- Fix type of monPred_bi_embedding and monPred_sbi_embedding. · ad06e03a
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  ad06e03a
- Embedding stuff in a separated file. · 86bb4fb3
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  86bb4fb3
- Fix iStartProof. · 8a9515b0
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  8a9515b0
- More instances for monPred. · 8ca83760
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  8ca83760
- Add lemma monPred_car_embed. · 66a41586
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  66a41586
- Renaming : morphism -> embedding. · 39967f22
  Jacques-Henri Jourdan authored Dec 13, 2017
  
  39967f22
- Add a bunch of proofmode instances for monPred_car and morphisms. · 858d6407
  Jacques-Henri Jourdan authored Dec 13, 2017
  
  858d6407
- Force all the BI morphisms to use the ⎡P⎤ notation. · cedd9645
  Jacques-Henri Jourdan authored Dec 12, 2017
  
  cedd9645
- Move stuff around. · 9c68a663
  Jacques-Henri Jourdan authored Dec 11, 2017
  
  9c68a663
- eta-expand bi_mor_exist and bi_mor_forall. · e2e8748f
  Jacques-Henri Jourdan authored Dec 11, 2017
  
  e2e8748f
- refactor : mor -> f · 1f9e71cf
  Jacques-Henri Jourdan authored Dec 11, 2017
  
  1f9e71cf
- Try on BI morphisms. · db2d9d6b
  Jacques-Henri Jourdan authored Dec 06, 2017
  
  db2d9d6b
- Tweak. · eb203c6b
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  eb203c6b
- minor renaming. · c1196f5e
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  c1196f5e
- Renaming monPred_ofe -> monPredC. · 66cb81f2
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  66cb81f2
- Add Inhabited in bi_index. · 3570accc
  Jacques-Henri Jourdan authored Dec 18, 2017
  
  3570accc
- MonPred.unseal in a module. · 4ad2b78f
  Jacques-Henri Jourdan authored Dec 14, 2017
  
  4ad2b78f
- Moved BiEmbedding, B->PROP for Bi name. · 5f9a2320
  Jacques-Henri Jourdan authored Dec 06, 2017
  
  5f9a2320
- Add typeclass for BI embeddings. · 45cf81a3
  Jacques-Henri Jourdan authored Dec 05, 2017
  
  45cf81a3
- Add a few missing instances. · 1e9c218f
  Jacques-Henri Jourdan authored Dec 04, 2017
  
  1e9c218f
- Use \Phi instead of P. · c2198d46
  Jacques-Henri Jourdan authored Dec 02, 2017
  
  c2198d46
- Other improvements. · 3d0430b6
  Jacques-Henri Jourdan authored Dec 02, 2017
  
  3d0430b6