xuanruiqi

12月 04 04:26:44 xuanrui systemd[1]: Started Firmware update daemon.
12月 04 04:27:01 xuanrui fwupd[17170]: 19:27:01:0292 FuContext            battery level now 90
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPlugin             add_security_attrs(acpi_dmar)
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuCommon             reading /sys/firmware/acpi/tables/DMAR with 184 bytes
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPluginAcpiDmar     OemTableId: Dell Inc
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPluginAcpiDmar     CreatorId:
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPluginAcpiDmar     Flags: 0x05
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPlugin             add_security_attrs(acpi_facp)
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuCommon             reading /sys/firmware/acpi/tables/FACP with 276 bytes
12月 04 04:27:24 xuanrui fwupd[17170]: 19:27:24:0583 FuPluginAcpiFacp     Flags: 0x20c4f5

xuanruiqi

+__rvm_remove_path_list_remove:2> typeset __item
+__rvm_remove_path_list_remove:3> __item=/home/xuanrui/.rvm/gems/ruby-2.6.3
+__rvm_remove_path_list_remove:5> printf 'Removing /home/xuanrui/.rvm/gems/ruby-2.6.3 - '
Removing /home/xuanrui/.rvm/gems/ruby-2.6.3 - +__rvm_remove_path_list_remove:6> __rvm_rm_rf /home/xuanrui/.rvm/gems/ruby-2.6.3
+__rvm_rm_rf:2> __rvm_rm_rf_verbose /home/xuanrui/.rvm/gems/ruby-2.6.3
+__rvm_rm_rf_verbose:2> typeset target
+__rvm_rm_rf_verbose:3> target=/home/xuanrui/.rvm/gems/ruby-2.6.3 
+__rvm_rm_rf_verbose:7> [[ -n 5.8 ]]
+__rvm_rm_rf_verbose:9> setopt extendedglob
+__rvm_rm_rf_verbose:17> case /home/xuanrui/.rvm/gems/ruby-2.6.3 (*(/|.)@(|/Applications|/Developer|/Guides|/Information|/Library|/Network|/System|/User|/Users|/Volumes|/backups|/bdsm|/bin|/boot|/cores|/data|/dev|/etc|/home|/lib|/lib64|/mach_kernel|/media|/misc|/mnt|/net|/opt|/private|/proc|/root|/sbin|/selinux|/srv|/sys|/tmp|/usr|/var))

xuanruiqi

(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.

xuanruiqi

Require Import Structures.Orders Nat.
From Equations Require Import Equations.

Set Implicit Arguments.

Module Tree (X : OrderedTypeFull').

  Include X.
    
  Inductive color := Red | Black.

xuanruiqi

Require Import Structures.Orders Nat.
From Equations Require Import Equations.

Set Implicit Arguments.

Module Tree (X : OrderedTypeFull').

  Include X.
    
  Inductive color := Red | Black.

xuanruiqi

{-# LANGUAGE GADTs, DataKinds, PolyKinds, InstanceSigs, KindSignatures, RankNTypes, TypeApplications #-}

data Ty = I | Arrow Ty Ty

data STy :: Ty -> * where
  ISing :: STy I
  ArrowSing :: STy s -> STy t -> STy (Arrow s t)

data Tm (var :: Ty -> *) :: Ty -> * where
  Const :: Integer -> Tm var I

xuanruiqi

Require Import Coq.Lists.List.

Set Implicit Arguments.

Inductive type : Set :=
| TNat : type
| TArrow : type -> type -> type.

Definition ctx := list type.

xuanruiqi

module rec M : sig
  type int_expr = [ `I of int | `Add of int_expr * int_expr ]
  and  bool_expr = [ `B of bool | `Eq of M.expr * M.expr ]

  type expr = [ int_expr | bool_expr ]
end = M

type result = ResI of int | ResB of bool

let compare_result (r : result) (r' : result) : bool =

xuanruiqi

Require Coq.Bool.Bool. Open Scope bool.
Require Import String.
Require Import Coq.Strings.Ascii. Open Scope char_scope.
Require Coq.Arith.PeanoNat. Open Scope nat_scope.
Require Coq.Lists.List. Open Scope list_scope.
Require Import BinInt.
Require Extraction.

Set Implicit Arguments.
Unset Elimination Schemes.

xuanruiqi

open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Relation.Binary
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym)
open Eq.≡-Reasoning
open import Data.Vec hiding (insert)
open import Data.Product

module TwoThree