Will Thomas
Will Thomas
I am trying to reduce the number of shrinks that QuickChick will run. Using the method outlined [here](https://softwarefoundations.cis.upenn.edu/qc-current/QuickChickInterface.html#lab129) I have `Extract Constant defNumShrinks => "0".` However, when I run `QuickChick...
The changes I have proposed in the pull request are adding an option to _CoqProjects of the form `-L `. This option will be interpreted by the coq_makefile to go...
This PR adds a "interpret to next point" that will take the current cursor position and if it is part of a tactic then it will interpret through the completion...
The processing of a command such as `debug auto` on: ``` Lemma test : forall A B C : Prop, (A -> B) -> (B -> C) -> (A ->...
_CoqProject: ``` -R . Test Test1.v Test2.v Test3.v ``` Test1.v: ``` Definition thing (x: nat) : nat := x. ``` Test2.v: ``` Require Import Test1. ``` Test3.v: ``` Require Import...
Main Highlights: 1. Yarn scripts for running the prettifier (in-place prettifies files) and linter 2. Linter made stricter 3. Typechecker made stricter (no explicit typecasting with `as`, tries to force...
Throughout I am utilizing CakeML v2274. Given two programs, one with and one without nested parentheses in case statements: ```sml fun fib n = case (n = 1) of True...
The spec for when the extension sidebar button appears (as laid out in #1028) says that the sidebar button should appear whenever a `*.v` or `_CoqProject` file has focus. However,...
It would be a nice feature of the CakeML compiler for it to provide warning messages during compilation of possibly unintended behaviors. **Example:** ```sml fun is_upper_X str = let val...