| 9d7c744 | Gregory Malecha | 03 April 2015, 06:49:30 UTC | a few more lemmas for Data.Prop. | 03 April 2015, 06:49:30 UTC |
| 49778e3 | Gregory Malecha | 03 April 2015, 06:20:20 UTC | A few more proofs. | 03 April 2015, 06:24:35 UTC |
| ac569fb | gregory malecha | 08 January 2015, 00:37:53 UTC | printString in the printing example. | 08 January 2015, 00:37:53 UTC |
| bd1caa9 | Gregory Malecha | 07 January 2015, 03:15:41 UTC | a simple example for printing. | 07 January 2015, 03:15:41 UTC |
| ab28e47 | Gregory Malecha | 06 December 2014, 04:29:42 UTC | adding eq_sym_eq_sym to Data.Eq. | 06 December 2014, 04:29:42 UTC |
| 229e122 | Gregory Malecha | 14 November 2014, 06:15:28 UTC | moving some lemmas. | 14 November 2014, 06:15:28 UTC |
| 1278812 | Gregory Malecha | 06 November 2014, 03:45:42 UTC | adding lazy list. | 06 November 2014, 03:45:42 UTC |
| 442c7e0 | Gregory Malecha | 05 November 2014, 18:55:29 UTC | more consistent naming in Data.Prop. | 05 November 2014, 18:55:29 UTC |
| c32e340 | Gregory Malecha | 05 November 2014, 18:33:32 UTC | more definitions! | 05 November 2014, 18:33:32 UTC |
| b5e3433 | Gregory Malecha | 03 November 2014, 05:29:35 UTC | injective instances for List. | 03 November 2014, 05:29:35 UTC |
| 5faa035 | Gregory Malecha | 21 October 2014, 20:29:25 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 21 October 2014, 20:29:25 UTC |
| fae710a | Gregory Malecha | 21 October 2014, 20:29:12 UTC | example of monad reasoning. | 21 October 2014, 20:29:12 UTC |
| c2c71a2 | Gregory Malecha | 09 October 2014, 12:31:37 UTC | Merge pull request #8 from clarus/master Bug fixes for conversions from integers to strings. | 09 October 2014, 12:31:37 UTC |
| 56295f9 | Guillaume Claret | 09 October 2014, 11:04:12 UTC | digit2ascii function fixed | 09 October 2014, 11:04:12 UTC |
| 0039176 | Guillaume Claret | 09 October 2014, 11:03:40 UTC | nat2string function fixed | 09 October 2014, 11:03:40 UTC |
| f6da121 | Gregory Malecha | 05 October 2014, 03:19:38 UTC | modifying the definition of equivalence of options. | 05 October 2014, 03:19:38 UTC |
| c8826ea | Gregory Malecha | 28 September 2014, 23:20:31 UTC | implementation of SumN. | 28 September 2014, 23:20:31 UTC |
| 0fe7953 | Gregory Malecha | 22 September 2014, 02:40:32 UTC | hrel and flip | 22 September 2014, 02:40:32 UTC |
| cf21029 | Gregory Malecha | 19 September 2014, 20:01:29 UTC | heterogenous relatedness when the relations are the same implies homogeneous relatedness | 19 September 2014, 20:01:29 UTC |
| f2cfd3e | Gregory Malecha | 19 September 2014, 19:57:46 UTC | heterogeneous relations on hlists | 19 September 2014, 19:57:46 UTC |
| 1b16f84 | Gregory Malecha | 19 September 2014, 17:25:38 UTC | lemmas about equiv_hlist. | 19 September 2014, 17:25:38 UTC |
| 28b4161 | Gregory Malecha | 18 September 2014, 19:35:11 UTC | implicit arguments to mapT_list. | 18 September 2014, 19:35:11 UTC |
| d8d091f | Gregory Malecha | 18 September 2014, 17:34:14 UTC | cleaner definition of list traverse | 18 September 2014, 17:34:14 UTC |
| a535a93 | Gregory Malecha | 15 September 2014, 00:52:22 UTC | implementation of Sum. | 15 September 2014, 00:52:22 UTC |
| 5c27c83 | Gregory Malecha | 12 September 2014, 20:26:22 UTC | Equational reasoning for Prop in Data.Prop | 12 September 2014, 20:26:22 UTC |
| 8e54e77 | Gregory Malecha | 07 August 2014, 02:04:20 UTC | Dead code in Data.Prop. | 07 August 2014, 02:04:20 UTC |
| e361819 | Gregory Malecha | 06 August 2014, 20:28:38 UTC | this is not provable without decidable equality. | 06 August 2014, 20:28:38 UTC |
| 47d1155 | Gregory Malecha | 01 August 2014, 22:15:37 UTC | Remove ListNth's and Show's dependence on omega. | 01 August 2014, 22:15:37 UTC |
| e04ba49 | Gregory Malecha | 01 August 2014, 20:30:08 UTC | don't add a rewrite for symmetry. | 01 August 2014, 20:30:08 UTC |
| 28cafe6 | Gregory Malecha | 01 August 2014, 19:33:38 UTC | Clean up for some eq_ lemmas - eq_option_eq moved to Data.Option - eq_list_eq added to Data.List - Changed Tactics.Equality to contain rewrites for Data.Eq - Building rewrite database for eq_matches | 01 August 2014, 19:33:38 UTC |
| 3ba620d | Gregory Malecha | 30 July 2014, 00:07:22 UTC | Removing EqDec requirements from Hcons inversion. | 30 July 2014, 00:07:22 UTC |
| 78d4433 | Gregory Malecha | 28 July 2014, 15:54:19 UTC | "f_equal" for matches. | 28 July 2014, 15:54:19 UTC |
| d4fe117 | Gregory Malecha | 28 July 2014, 15:53:57 UTC | adding injective instance for S | 28 July 2014, 15:53:57 UTC |
| 42d55a5 | Gregory Malecha | 18 July 2014, 23:26:49 UTC | Lemmas about matching on pf and then eq_sym pf. | 18 July 2014, 23:26:49 UTC |
| 370994c | Gregory Malecha | 08 July 2014, 13:23:44 UTC | remove EqDec requirement for hlist_nth_hlist_app - transparent proofs make all the difference. | 08 July 2014, 13:23:44 UTC |
| 7c5ce6c | Gregory Malecha | 18 June 2014, 17:09:49 UTC | Fun is an applicative. | 18 June 2014, 17:09:49 UTC |
| bf4e713 | Gregory Malecha | 18 June 2014, 03:53:16 UTC | well_founded relations are Irreflexive | 18 June 2014, 03:53:16 UTC |
| 5d9238a | Gregory Malecha | 14 June 2014, 22:17:51 UTC | change_rewrite | 14 June 2014, 22:17:51 UTC |
| b2303cd | Gregory Malecha | 10 June 2014, 17:15:48 UTC | Adding nth_error_length_lt = Fixing imports | 10 June 2014, 17:15:48 UTC |
| d912f9c | Gregory Malecha | 29 May 2014, 14:19:02 UTC | Adding ExtLib.Data.Member. - One proof seems to require UIP_refl, perhaps there is a way around this? | 29 May 2014, 14:19:02 UTC |
| 338dfc1 | Gregory Malecha | 26 May 2014, 13:57:59 UTC | lemmas for manipulating matches on eq. | 26 May 2014, 13:57:59 UTC |
| a7a437e | Gregory Malecha | 08 May 2014, 19:44:42 UTC | a more useful hlist_app_nil_r. | 08 May 2014, 19:44:42 UTC |
| 5427df3 | Gregory Malecha | 08 May 2014, 18:52:52 UTC | hlist_app_nil_r. | 08 May 2014, 18:52:52 UTC |
| 95de1b3 | Gregory Malecha | 07 May 2014, 23:04:21 UTC | removing some dependence on decidable equality. | 07 May 2014, 23:04:21 UTC |
| 9fe9db6 | Gregory Malecha | 30 April 2014, 02:00:05 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 30 April 2014, 02:00:05 UTC |
| 7752939 | Gregory Malecha | 30 April 2014, 01:59:16 UTC | removing an old comment. | 30 April 2014, 01:59:16 UTC |
| 695e176 | gregory malecha | 28 April 2014, 03:19:47 UTC | adding FunctorLaws. | 28 April 2014, 03:19:47 UTC |
| 9f2ce47 | Gregory Malecha | 09 April 2014, 21:33:21 UTC | starting to make consistent with coq trunk. | 09 April 2014, 21:33:21 UTC |
| c18fee9 | Gregory Malecha | 06 April 2014, 16:21:32 UTC | working on what match means. | 06 April 2014, 16:21:32 UTC |
| 8b39fdd | Gregory Malecha | 05 April 2014, 16:27:41 UTC | Improvements to Data to support dependency | 05 April 2014, 16:27:41 UTC |
| 67656f5 | Gregory Malecha | 27 March 2014, 10:11:11 UTC | functions to well-founded spaces are well-founded. | 27 March 2014, 10:11:11 UTC |
| bfa37d2 | Gregory Malecha | 27 March 2014, 10:10:44 UTC | a setoid version of the fixpoint equation. | 27 March 2014, 10:10:44 UTC |
| d29142d | Gregory Malecha | 23 March 2014, 07:37:38 UTC | remove need for decidable equality. | 23 March 2014, 07:37:38 UTC |
| b0f8ec3 | Gregory Malecha | 03 March 2014, 23:33:22 UTC | fixing the order of arguments for function composition. | 03 March 2014, 23:33:22 UTC |
| 8f5b0ea | Gregory Malecha | 27 February 2014, 21:35:45 UTC | Adding a simple forward reasoning tactic. | 27 February 2014, 21:35:45 UTC |
| 06afdf7 | Gregory Malecha | 22 February 2014, 01:37:48 UTC | avoid 'run' because it seems to be part of Mtac | 22 February 2014, 01:37:48 UTC |
| 4af1a22 | Gregory Malecha | 22 February 2014, 01:37:36 UTC | whitespace in Structures.Monad. | 22 February 2014, 01:37:36 UTC |
| 56bde82 | Gregory Malecha | 22 February 2014, 01:36:54 UTC | Lazy is a monad, but I don't recommend you use it. | 22 February 2014, 01:36:54 UTC |
| 9f47f94 | Gregory Malecha | 19 December 2013, 04:19:39 UTC | Laziness is important for getting good computational behavior. | 19 December 2013, 04:19:39 UTC |
| dfee798 | Gregory Malecha | 19 December 2013, 03:12:14 UTC | some extra monad instances. | 19 December 2013, 03:12:14 UTC |
| d93ba5d | Gregory Malecha | 18 December 2013, 20:59:05 UTC | implicit arguments on mjoin | 18 December 2013, 20:59:05 UTC |
| cd5dc04 | Gregory Malecha | 16 December 2013, 17:23:03 UTC | an uninstall rule. | 16 December 2013, 17:23:03 UTC |
| caf1165 | Gregory Malecha | 16 December 2013, 17:14:35 UTC | adding an uninstall target to the Makefile - Also, fixed UsingSets example. | 16 December 2013, 17:14:35 UTC |
| f4c6198 | gregory malecha | 27 November 2013, 21:49:06 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 27 November 2013, 21:49:06 UTC |
| 5ee5228 | gregory malecha | 27 November 2013, 21:48:18 UTC | fixing rewrite_all & new function in hlist | 27 November 2013, 21:48:18 UTC |
| bdc1d38 | Gregory Malecha | 27 November 2013, 19:44:07 UTC | removing broken dependencies on Logic. - In the future, Logic will be pulled in through Charge. | 27 November 2013, 19:45:09 UTC |
| 44162b2 | Gregory Malecha | 26 November 2013, 04:51:15 UTC | removing Structures.Logic (will use Charge!) | 26 November 2013, 04:51:15 UTC |
| a18a955 | gregory malecha | 19 November 2013, 01:08:31 UTC | more variants of rewrite_all (I should find notation for this) | 19 November 2013, 01:08:31 UTC |
| 27409f5 | gregory malecha | 19 November 2013, 01:06:29 UTC | fixing rewrite_all to work in the hypotheses as well. | 19 November 2013, 01:06:29 UTC |
| 5828f48 | Gregory Malecha | 18 November 2013, 02:47:50 UTC | well-foundedness of leftTrans. | 18 November 2013, 02:47:50 UTC |
| aeb6399 | Gregory Malecha | 18 November 2013, 02:38:44 UTC | left step for right transitivity. | 18 November 2013, 02:38:44 UTC |
| 50137fd | Gregory Malecha | 15 November 2013, 21:23:52 UTC | adding hlist_rev to HList. | 15 November 2013, 21:23:52 UTC |
| 1624806 | Gregory Malecha | 12 November 2013, 15:59:46 UTC | Injective for pairs. | 12 November 2013, 15:59:46 UTC |
| 7218453 | Gregory Malecha | 11 November 2013, 23:50:49 UTC | Fix_equiv, a generalization of Fix_eq over arbitrary relations. | 11 November 2013, 23:50:49 UTC |
| 93d6139 | gregory malecha | 07 November 2013, 15:57:08 UTC | a few bug fixes to EqDep. | 07 November 2013, 15:57:08 UTC |
| 6f60650 | Gregory Malecha | 07 November 2013, 14:25:12 UTC | inv_all now breaks apart exists facts. | 07 November 2013, 14:25:12 UTC |
| 9b76bab | Gregory Malecha | 06 November 2013, 19:48:46 UTC | adding an export module for common tactics. | 06 November 2013, 19:48:46 UTC |
| 535fdd7 | Gregory Malecha | 04 November 2013, 04:18:11 UTC | the other direction of hlist_app_assoc. - they aren't proved simultaneously because of the cast | 04 November 2013, 04:18:11 UTC |
| b46e2b2 | Gregory Malecha | 04 November 2013, 02:45:04 UTC | a few more instances to Nat. | 04 November 2013, 02:45:04 UTC |
| 92fcc02 | Gregory Malecha | 04 November 2013, 02:41:38 UTC | removing dependency on Show. | 04 November 2013, 02:41:38 UTC |
| bee9cf5 | Gregory Malecha | 04 November 2013, 02:33:59 UTC | additions to FMapPositive but not quite usable yet | 04 November 2013, 02:33:59 UTC |
| 4e6e4fb | Gregory Malecha | 02 November 2013, 03:53:04 UTC | adding Functor instance to Option and FMapPositive. | 02 November 2013, 03:53:04 UTC |
| e4abdcd | Gregory Malecha | 01 November 2013, 21:28:24 UTC | proof of MapOk for FMapPositive. | 01 November 2013, 21:28:24 UTC |
| 9212b20 | Gregory Malecha | 01 November 2013, 16:07:43 UTC | hlist_split and its interaction with hlist_app. | 01 November 2013, 16:07:43 UTC |
| 8aa1e86 | Gregory Malecha | 01 November 2013, 15:40:57 UTC | adding hlist_app_assoc. | 01 November 2013, 15:40:57 UTC |
| b2cc16a | Gregory Malecha | 01 November 2013, 15:29:03 UTC | cleaning up ghost dependencies. | 01 November 2013, 15:29:03 UTC |
| 6770ddf | Gregory Malecha | 28 October 2013, 13:51:50 UTC | a few more tactics for doing case analysis. | 28 October 2013, 13:51:50 UTC |
| c117b8f | Gregory Malecha | 26 October 2013, 03:11:51 UTC | unfolding hints for rel_dec + symmetry lemma | 26 October 2013, 03:11:51 UTC |
| 5c8d2a8 | Gregory Malecha | 18 October 2013, 18:41:02 UTC | fixes to RelDec and Consider. - move "default" instances of RelDec (Sum still remains) - remove dependency of RelDec on Consider - remove example from Consider to avoid pulling in Omega | 18 October 2013, 18:57:53 UTC |
| f16efa2 | Gregory Malecha | 08 October 2013, 16:15:21 UTC | Adding a functor instance for FMapAList. | 08 October 2013, 16:15:21 UTC |
| d3e04b4 | Gregory Malecha | 06 October 2013, 15:23:38 UTC | make injection do the right thing for /\ - There is possibly a better way to do this by exposing the conjunctions (possibly as dependent sums) and then reflecting the destruction of this. | 06 October 2013, 15:23:38 UTC |
| c45c4d4 | Gregory Malecha | 05 October 2013, 03:23:23 UTC | adding a very weak Foldable law. | 05 October 2013, 03:23:23 UTC |
| 80a6404 | Gregory Malecha | 24 August 2013, 23:58:02 UTC | adding gen_refl tactic. | 24 August 2013, 23:58:02 UTC |
| 9b47ed3 | Gregory Malecha | 23 August 2013, 04:06:44 UTC | adding Checked which implements a dependent option type. | 23 August 2013, 04:06:44 UTC |
| 546557a | Gregory Malecha | 09 August 2013, 03:06:15 UTC | whitespace issues in fmap positive. | 09 August 2013, 03:06:15 UTC |
| 80a3ad7 | Gregory Malecha | 31 July 2013, 21:35:55 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 31 July 2013, 21:35:55 UTC |
| da26c42 | Gregory Malecha | 31 July 2013, 21:35:26 UTC | adding a few new instances for HList. | 31 July 2013, 21:35:26 UTC |
| 81d874d | Scott Moore | 31 July 2013, 17:09:57 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 31 July 2013, 17:09:57 UTC |
| c5da32d | Scott Moore | 31 July 2013, 17:09:28 UTC | RelDec and Injective instances for Fin | 31 July 2013, 17:09:28 UTC |
| 4d55251 | Gregory Malecha | 30 July 2013, 20:22:15 UTC | Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib | 30 July 2013, 20:22:15 UTC |
