erutuf

Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

erutuf

Require Import Arith.
Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

erutuf

Require Import Program.Basics.
Require Import Arith.Le.
Require Import Omega.
Require Import Classes.Equivalence.
Require Import Classes.SetoidClass.

Set Implicit Arguments.
Unset Strict Implicit.

erutuf

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_S : forall n, even n -> odd (S n).

Scheme even_mut := Induction for even Sort Prop
  with odd_mut := Induction for odd Sort Prop.

Theorem daigakuseinosuugakuryoku : forall n m, 

erutuf

Require Import List.
Require Import Bool.
Require Import Bool.Sumbool.

Ltac find_if :=
  match goal with
  | H:context[if ?X then _ else _] |- _ => destruct X as ()_eqn
  | |- context[if ?X then _ else _] => destruct X as ()_eqn
  end.

erutuf

open List;;

let rec seq n m = if n > m then [] else n :: seq (n + 1) m;;

let rec safe x n = function
    | [] -> true
    | y::ys -> x <> y && x <> y + n && x <> y - n && safe x (n + 1) ys;;

let concmap f xs = concat (map f xs)

erutuf

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩ ☜_☞

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse

erutuf

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse

erutuf

module HaityuuOishii where

data False : Set where

data _\/_ (P Q : Set) : Set where
    orl : P -> P \/ Q
    orr : Q -> P \/ Q

haityu : (P : Set) -> (forall (P : Set) -> ((P -> False) -> False) -> P) -> (P \/ (P -> False))
haityu P nnp = nnp (P \/ (P -> False)) (\ z -> z ((orr (\ x -> z (orl x)))))

erutuf

{-# OPTIONS --universe-polymorphism #-}

module Msort where

open import Level
open import Data.Nat
open import Data.Sum 
open import Data.Unit
open import Data.Empty