Junyoung/"Clare" Jang
Junyoung/"Clare" Jang
It would be useful (especially for testing) to add some commands that control whether harpoon saves finished session automatically or not. However, to safely defer saving, harpoon should store finished...
IMO, Current code style is sufficiently inconsistent to introduce a tool for managing it. ~I found that ocamlformat is not so bad in terms of the number of options, reliability,...
[The last theorem](https://github.com/Beluga-lang/Beluga/blob/f7d0d7a8ee39967fd0f88064163e7e90ef17f68d/t/harpoon/poplmark-reloaded/props.input#L205-L225) of f7d0d7a8ee39967fd0f88064163e7e90ef17f68d, namely ``` anti-renameSN {g : cxt} {g' : cxt} {$R : [g' |-# g]} {M : [g |- tm A[]]} SN [g' |- M[$R]] ->...
As a demonstration, when I have these holes, ``` %coverage LF ty : type = | base : ty | arr : ty -> ty -> ty ; %name ty...
With the next beluga code and input, harpoon consumes indefinite amount of time to finish. ``` % nats_and_bools_tps.bel LF term : type = | true : term | false :...
Link: https://www.ctan.org/pkg/bussproofs Even though it is possible to write simple inference rules and logical proofs with `array` env and `\frac`, `\cfrac`, etc., it becomes significantly hard to write complex rules...
Is there any official benchmark comparing Capability with other libraries, for example, mtl? If there's none, is there any plan to provide one?
Will it be possible to support logos of https://coq.inria.fr/ and https://agda.readthedocs.io/en/v2.6.1.3/ ? They are both quite famous proof assistants, so it will be great if the support is possible.
When there is a definition like ```Haskell myFun :: a -> a -> a -> a -> a -> a -> a -> a -> a -> a -> a...