Beluga

Beluga copied to clipboard

I try to write as much code documentation as I can. It would be great if we could integrate OCamldoc into the mix so that we can generate HTML documentation...

tsani

Unbound variable

1

Load this signature. ``` kind : type. con : type. lam : kind -> (con -> con) -> con. app : con -> con -> con. cn-of : con ->...

tsani

Loading this signature in Harpoon: ``` LF nat : type = | zero : nat | succ : nat -> nat ; --name nat N. LF lt : nat ->...

MartyO256

Type erasure issue in translated program from Harpoon proof

1

Load the following signature: ``` LF kind : type = sigma : kind -> (con -> kind) -> kind and con : type =; LF kind-eq : kind -> kind...

MartyO256

Wrong error message on recursive call using unbound meta-level identifier

1

Load the following signature: ``` LF nat : type = | z : nat | s : nat → nat ; LF leq : nat → nat → type =...

MartyO256

Termination checking for complete induction

1

Twelf has a [reduction declaration](https://www.cs.cmu.edu/~twelf/guide-1-4/twelf_8.html#SEC47) that can be used to label the outputs of lemmas as non-inflationary, which allows for recursive calls on these outputs. Totality checking for such programs...

MartyO256

Cannot use overshadowed LF type in proofs declared prior to the overshadowing

4

Load the following signature: ``` LF term : type =; LF term-eq : term -> term -> type = | term-eq/i : term-eq M M ; proof term-resp-term : {...

MartyO256

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...

Ailrun

Introduce an automatic code style formatter

2

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,...

Ailrun

Harpoon removes a substitution variable from the scope when splitting on a variable using the substitution

2

[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]] ->...

Ailrun