advancedresearch/hooo issues and pull requests

#145 - Added info about "hooo-meta_cache.bin"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#144 - Added meta cache

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#143 - Fixed rules numbers in syntax

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#142 - Remove `<prove>;` syntax

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#141 - Declare symbols

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#140 - Parse type judgement

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#139 - Improved function and lambda syntax

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#138 - Fixed docs

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#137 - Added more docs

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#136 - Make solver stricter

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#135 - Use std axioms in "std/hooo.hooo"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#134 - Added symbolic distinction

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#133 - Add symbolic distinction

Issue - State: closed - Opened by bvssvni over 1 year ago - 1 comment
Labels: hard

#132 - Type level type judgement

Issue - State: closed - Opened by bvssvni over 1 year ago - 1 comment
Labels: hard

#131 - Declare symbols to avoid needing ad-hoc notation

Issue - State: closed - Opened by bvssvni over 1 year ago
Labels: hard

#130 - Published 0.2.5

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#129 - Allow quantification over application

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#128 - Make all use of symbols explicit

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#127 - Renamed to "nat_add_ty"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#126 - Added "add_ty"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#125 - Added symbols to docs

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#124 - Fixed typos in docs

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#123 - Added "std/nat.hooo"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#122 - Published 0.2.4

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#121 - Improved type check error messages

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#120 - Added "pow_modus_tollens"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#119 - Added "modal_tauto_t_to_para_nec_false"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#118 - Fixed N, renamed old axiom to N2

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#117 - Improved parsing

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#116 - Improved parsing

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#115 - Fix `tauto_hooo_imply` in README and docs

Issue - State: closed - Opened by bvssvni over 1 year ago - 1 comment
Labels: bug

#114 - Added "modal_n_to_nlob"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#113 - Added more stuff to "std"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#112 - Added normal congruence for `□` and `◇`

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#111 - Fixed some modal stuff

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#110 - Added some modal stuff

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#109 - Use lazy_static for match type

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#108 - Published 0.2.3

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#107 - Parallelize type checking

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#106 - Added more stuff to "std"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#105 - Improved parsing

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#104 - Use lazy_static

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#103 - Added more stuff to "std"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#102 - Added some refl stuff

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#101 - Added `tauto_nnexcm`

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#100 - Added more stuff to "qu"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#99 - Added "modus_tollens"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#98 - Added "q_left" and "q_right"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#97 - Added more stuff to "qu"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#96 - Display multi app

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#95 - Improved parsing

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#94 - Added symbols and application

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#93 - Symbols design

Issue - State: open - Opened by bvssvni over 1 year ago
Labels: draft, discussion

#92 - Improved syntax

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#91 - Fixed syntax

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#90 - Added `=^=` syntax sugar

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#89 - Added some theorems to "std/hooo.hooo"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#88 - Improved error message

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#87 - Published 0.2.2

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#86 - Handle contravariance

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#85 - Added explicit `all(..)`

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#84 - Add explicit `all(..)`

Issue - State: closed - Opened by bvssvni over 1 year ago
Labels: hard

#83 - Fixed display of "^" and "!"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#82 - Improved display of "excm"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#81 - Improved display of "=="

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#80 - Improved display of "!"

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#79 - Soundness of `all(..)`

Issue - State: open - Opened by bvssvni over 1 year ago - 1 comment
Labels: draft, discussion

#78 - Fixed some typos

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#77 - Fixed some typos

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#76 - Published 0.2.1

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#75 - Fixed docs

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#74 - Redesign

Pull Request - State: closed - Opened by bvssvni over 1 year ago

#73 - Redesign

Issue - State: closed - Opened by bvssvni over 1 year ago
Labels: hard

#72 - Replace wave operator with symmetric normal path by `not`

Issue - State: closed - Opened by bvssvni over 2 years ago - 1 comment
Labels: draft, discussion

#71 - Fix dual of `eq`

Issue - State: closed - Opened by bvssvni over 2 years ago - 1 comment
Labels: draft, discussion

#70 - Fix dual of `imply`

Issue - State: closed - Opened by bvssvni over 2 years ago - 1 comment
Labels: draft, discussion

#69 - Check soundness of exponential sub-expressions

Issue - State: closed - Opened by bvssvni over 2 years ago - 1 comment
Labels: discussion

#68 - Add wave operator for unary operator duality?

Issue - State: closed - Opened by bvssvni over 2 years ago - 1 comment
Labels: discussion

#67 - Can exponentials model modality?

Issue - State: closed - Opened by bvssvni over 2 years ago
Labels: discussion

#66 - Unification of lambdas and dependent types as exponentials

Issue - State: closed - Opened by bvssvni over 2 years ago
Labels: discussion

#65 - Shared context vs application

Issue - State: closed - Opened by bvssvni over 2 years ago - 2 comments
Labels: discussion

#64 - Removed `((A ^ B) → (A → B))`

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#63 - Application substitution

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#62 - Add exponent as context

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#61 - Added higher order suggestions for all tactics

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#60 - Rewriting in left and right argument of pow

Issue - State: closed - Opened by bvssvni over 2 years ago - 2 comments
Labels: draft, discussion

#59 - Don't rewrite in left or right argument of the power operator

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#58 - Lift equality reflexivity in "hooo" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#57 - Improved "imply" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#56 - Added "source/hooo/lower_true.hooo"

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#55 - Improved "hooo" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#54 - Rename `refl` to `hooo_refl`

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#53 - Fixed comment

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#52 - Improved "hooo" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#51 - Improved "imply" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#50 - Improved "hooo" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#49 - Added lift to "qual" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#48 - Improved "or" tactic

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#47 - Added "theory" symbol

Pull Request - State: closed - Opened by bvssvni over 2 years ago

#46 - Simplified parsing of symbols

Pull Request - State: closed - Opened by bvssvni over 2 years ago

GitHub / advancedresearch/hooo issues and pull requests