小编Car*_*lin的帖子

我正在使用这篇博文中定义的自定义目标文件。在构建静态库时它工作得很好，但是当我尝试构建二进制文件时，我收到以下警告：

warning: dropping unsupported crate type `bin` for target `x86_64-unknown-none-gnu`

没有构建任何二进制文件。

如何向我的目标添加对构建可执行文件的支持？

MSets似乎是使用OCaml样式的有限集的方法。可悲的是，我找不到示例用法。

如何定义一个空的MSet或单例的MSet？如何将两个MSets结合在一起？

考虑以下玩具语法和解析器:

(* in EBNF:
  ap = "a", { "ba" }
  bp = ap, "bc"
*)
let ap = sepBy1 (pstring "a") (pstring "b")
let bp = ap .>> (pstring "bc")
let test = run bp "abababc"

我得到以下输出:

Error in Ln: 1 Col: 7
abababc
      ^
Expecting: 'a'

清楚地sepBy1看到最后一个b并期望它导致另一个a,当它找不到时失败.是否有一个变sepBy1体会回溯b并使这个解析成功？我不应该使用它吗？

class Foo[T](t: T)(implicit int: Numeric[T]) {
  val negated = -t
  val doubled = t + t
  val squared = t * t
  // ...
}

我在这里的所有三行上都有红色波浪线。是什么赋予了？

在我的机器上，我有一些卷，其名称看起来像散列。我不记得创建或使用它们。docker volume inspect表明它们是很久以前创建的。有什么方法可以检查它们上次使用的时间或用途吗？

我有以下代码test.s:

call $8 + $8

运行nasm test.s编译成功.我希望以下等效的Rust代码能够成功编译,但事实并非如此.

在test.rs:

#![feature(asm)]
fn main() {
    unsafe {
        asm! (
            "call $0 + $0"
            :
            : "i" (8)
            : "memory"
            : "volatile"
        )
    }
}

产量rustc test.rs:

test.rs:4:9: 10:11 error: <inline asm>:1:12: error: invalid token in expression
        call $8 + $8
                  ^

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  Fail checkForall H. (* not a forall *)
Abort.

我会天真地期望checkForall H成功,但事实并非如此.

在他的" 依赖类型认证编程"一书中,Adam Chlipala 讨论了依赖类型的模式匹配限制:

问题是统一变量可能不包含本地绑定变量.

这是我在这里看到的行为的原因吗？

我想出了以下玩具证明脚本：

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Unfold myValue.

Example test: myProp myValue.
Proof.
  auto 1000. (* does nothing *)
  unfold myValue.
  trivial.
Qed.

为什么我需要在myValue这里手动展开？提示是否足够？

我正在尝试自动化决定程序,以确定ASCII字符是否为空格.这是我现在拥有的.

Require Import Ascii String.

Scheme Equality for ascii.

Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).

Definition isWhitespace (c : ascii) : {IsWhitespace c} + {not (IsWhitespace c)}.
Proof.
  unfold IsWhitespace.
  pose proof (ascii_eq_dec c "009"%char) as [H1|H1];
  pose proof (ascii_eq_dec c "032"%char) as [H2|H2];
  auto.
  right. intros [H3|H3]; auto.
Admitted.

什么是使证明更简洁的好方法？

考虑以下:

type Properties = {
    foo: { n: number };
    bar: { s: string };
    baz: { b: boolean };
};

declare function retrieveValues<K extends keyof Properties>(add?: K[]): Pick<Properties, K>[K];

// what happens
const x: { n: number } | { s: string } = retrieveValues(['foo', 'bar']);

// what I'm really trying to express (type error)
const y: { n: number } & { s: string } = retrieveValues(['foo', 'bar']);

有没有办法得到一个属性的交集Pick<Properties, K>？或者只是根据数组中相关字符串的存在来获取一组类型的交集的另一种方法？

有时我会通过投射到不同的空间来做最好的证明.目前我做了以下事情:

remember (f x) as y eqn:H; clear H; clear x.

我尝试使用Ltac自动执行此操作:

Ltac project x y :=
  let z := fresh in
    remember x as y eqn:z; clear z; clear x.

但是我收到以下错误:

Error: Ltac variable x is bound to f x which cannot be coerced to a variable.

这是什么问题？

考虑以下部分证明：

Theorem test : forall (n m : nat),
  n = m -> S n = S m.
Proof.
  intros n m H.

执行到这一点给我以下内容：

1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m

我想S从目标中删除s ，获得目标n = m。有没有一种策略可以做到这一点？

考虑以下目标：

Goal forall (x y: I = I), x = y.
Proof.
Abort.

Goal forall (x y: tt = tt), x = y.
Proof.
Abort.

这两个I和tt是单类型的成员。前者住Prop，后者住Set。这些是非常简单的类型，因此我不希望它们在任何设置中都支持丰富的相等类型。这些目标是否可以在 Coq 中证明而不诉诸身份证明公理的唯一性？