小编FZe*_*Zed的帖子

使用DU(Discriminated Union类型),如何执行类型测试模式匹配？我有以下运行代码:

type IU =
|Int of int
|Unit of Unit

let x = IU.Int(3)
let y = IU.Unit(())
let z = [3.14]

let showI (v) = 
    match box v with
    | :? IU -> 
        match v with
        | Int(_) -> "an IU int"
        |_ -> "not a IU.int"
    |_ -> "not a IU.int"

但我对showI函数中的内部匹配不满意.我更喜欢这样的东西:

let showI (v) = 
    match box v with
    | :? IU.Int -> "an int"
    |_ -> "not a IU.int"

哪个不编译(错误:未定义Int类型).

我错过了明显的语法吗？谢谢.

注意:showI函数接受具有未知类型的变量; 这就是臭盒v的原因.

我已经安装了虞美人上mathcomp/SSreflect的顶部.

即使我还没有掌握标准Coq,我想用它进行非常基本的实际分析.

这是我的第一个引理:

Definition fsquare (x : R) : R := x ^ 2.
Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).

is_derive f x0 f'是一个Coquelicot Prop,它说明了函数的导数f at x0 is f'.

由于auto_deriveCoquelicot提供的策略,我已经证明了这个引理.

如果我想让我的手有点脏,这是我的尝试没有auto_derive:

Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).
Proof.
  move => y.
  unfold fsquare.
  evar_last.
  apply is_derive_pow.
  apply is_derive_id.
  simpl.

而现在我对这个未决的判决感到困惑:

1 subgoal
y : R_AbsRing
______________________________________(1/1)
2 * one * (y …

根据这个 kvb的答案,这段代码编译(F#4)并运行:

type Untupler = abstract Apply : 'u * 'u -> 'u

let myotherFun arg1 arg2 =
    printfn "myotherFun result is : %A %A" arg1 arg2

let myFunction tup1 tup2 (i:Untupler) =
    myotherFun (i.Apply tup1) (i.Apply tup2)

let reskvb = myFunction (1,2) ("Hello","World") { new Untupler with member __.Apply (x,y) = snd (x,y) }

但如果最后一行被初始答案取代:

let reskvb = myFunction (1,2) ("Hello","World") { new Untupler with member __.Apply x = fst x }

然后编译器抱怨错误FS0768: 成员'Apply'不接受正确数量的参数,预期有2个参数

我不明白为什么编译器似乎无法推断x确实是一个元组.还是我还缺少另一个问题？谢谢.

我得到了这个函数的警告:

let dayofW' (d:System.DateTime) =
  match d.DayOfWeek with
  | DayOfWeek.Sunday    -> 0.0
  | DayOfWeek.Monday    -> 1.0
  | DayOfWeek.Tuesday   -> 2.0
  | DayOfWeek.Wednesday -> 3.0
  | DayOfWeek.Thursday  -> 4.0
  | DayOfWeek.Friday    -> 5.0
  | DayOfWeek.Saturday  -> 6.0

不完整的模式匹配此表达式.例如,值'enum(7)'可以指示模式未涵盖的情况.

我知道我必须处理Enum(而不是DU),但我找不到办法.我在msdn语言参考中找不到"枚举模式".

如何以最小的过度劳累删除警告？

我使用以下方法从注册中标记a到标记的文本:br

 `a"ry`b

它排除了标记位置上的字符b.示例:

1234500000
^   ^
a   b

我报到1234了r.

当我猛拉时,我想将角色包含在标记b位置.所以我想12345进行注册r.

我该怎么办？(我想避免定位b到下一个0)