我正在尝试遵循基本的 react-build-app 教程。
环境
我在 Windows 10 上使用 Ubuntu。
节点版本：v13.3.0
NPM 版本：6.13.1
到目前为止，我做到了，
npm install -g create-react-app
create-react-app calculator
cd calculator
npm start
问题
当我运行 npm start 时，我从 Windows 弹出对话框说，Windows cannot find '\https://localhost:3000/\'. Make sure you typed the name correctly, and then try again.
这是错误的屏幕截图
但是，在 cli 中，我看到
Local: http://localhost:3000/
On Your Network: http://192.168.56.1:3000/
Note that the development build is not optimized.
To create a production build, use npm run build.```
但是当我打开浏览器并转到http://localhost:3000/ 时，我只看到一个空白页面，而不是正常的 React 徽标。
预期产出
转到 …
我有一个类型，比如说
Inductive Tt := a | b | c.
定义它的子类型的最简单和/或最好的方法是什么？假设我希望子类型仅包含构造函数a和b. 一种方法是对二元素类型进行参数化，例如 bool：
Definition filt (x:bool): Tt := match x with
| true => a
| false => b end.
Check filt true: Tt.
这是可行的，但如果您的表达式具有以这种方式定义的多个（可能相互依赖的）子类型，则非常尴尬。此外，它只能工作一半，因为没有定义子类型。为此我必须另外定义例如
Notation _Tt := ltac: (let T := type of (forall {x:bool}, filt x) in exact T).
Fail Check a: _Tt. (*The term "filt x" has type "Tt" which should be Set, Prop or Type.*)
在这种情况下也不起作用。另一种方法是使用类型类，例如
Class s_Tt: Type := s: Tt.
Instance …在命题和谓词演算中证明了数十个引理之后（有些比其他的更具挑战性，但通常仍然可以在intro-apply-destruct自动驾驶仪上证明），我从一开始就打了一个~forall，并立即被抓住了。显然，我对 Coq 的理解和知识缺乏。所以，我要求使用低级 Coq 技术来证明一般形式的语句
~forall A [B].., C -> D.
exists A [B].., ~(C -> D).
换句话说，我希望有一个通用的 Coq 方法来设置和触发反例。（量化上述函数的主要原因是它是 Coq 中的（或）原始连接词。）如果你想要例子，我建议例如
~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.
有一个相关的问题既没有提出也没有回答我的问题，所以我认为它不是重复的。
我可以查询可用的包，nix-env -qa [package]但是如何查找依赖于主包并且可以单独加载或安装的可选包（例如库）？例如：勒柯克（coq-8.6）的包coqPackages_8_6.ssreflect和coqPackages_8_6.mathcomp我可以得到没有关于尼克斯AFAIK信息