yoshihiro503

// すごいE本の30.6章の「選択的な節を持つ型」 (p.538) をScalaでも
object AlternativeClausesType {
  def main() = {
    val List(_, _) = convert(('a, 'b))
    val (_, _)     = convert(List('a, 'b))
    val List(_, _) = convert(List('a, 'b)) // <- 型エラーにできる
    val (_, _)     = convert(('a, 'b))     // <- 型エラーにできる
  }
  
  def convert(xy: (Symbol, Symbol)): List[Symbol] = xy match {

yoshihiro503

Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity.  Qed.

yoshihiro503

import scala.reflect.ClassTag

class EqualsWithOnlySameType[A <: EqualsWithOnlySameType[A] : ClassTag) {
  override def equals(other: Any): Boolean = {
    other match {
      case (otherA: A) => super.equals(otherA)
      case _ => throw new RuntimeException(s"異なる型同士の比較を禁止しています: $this.equals($other)")
    }
  }
}

yoshihiro503

val tup22 = (1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1)

val ((a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v), w) = (tup22, "hoge")

yoshihiro503

(**
 * 自然数の二進表現
 * 例: (10010) は O I O O I Z
 * 一つの数の表現が一意でないことに注意
 *)
Inductive bin_numb :=
  | I : bin_numb -> bin_numb
  | O : bin_numb -> bin_numb
  | Z : bin_numb.

yoshihiro503

Require Import Program Arith.

(** * リストモジュールの拡張 *)
Module List.
  Require Export List.
 
  Fixpoint _index_of_loop {A:Type} (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i :=
    match xs with
    | nil => None
    | x::xs => if eq_dec x a then Some i else _index_of_loop eq_dec a xs (S i)

yoshihiro503

Definition foo (b : bool) : nat =
  if b then 0 else 1.

yoshihiro503

  let '(x, y, z) := (1, 2, 3) in
  ...

yoshihiro503

-R src JapaneseCoqdocSampleProject
src/Hoge.v
src/Piyo.v
-custom "platex Proof.tex; platex Proof.tex" "Proof.tex $(VOFILES) $(VFILES:.v=.tex)" "Proof.dvi"
-custom "dvipdfmx Proof.dvi" "Proof.dvi" Proof.pdf

yoshihiro503

Lemma exo4 : False \/ True.
Proof.
  right. exact I.
Qed.