data _∨_ (P Q : Set) : Set where
  ∨-intro₀ : P -> P ∨ Q
  ∨-intro₁ : Q -> P ∨ Q   

∨-elim : ∀ {P Q} {R : Set} -> (P -> R) -> (Q -> R) -> (P ∨ Q -> R)

∨-elim pr _ (∨-intro₀ p) = pr p
∨-elim _ qr (∨-intro₁ q) = qr q 

data _∨_

_∨_

(P Q : Set) : Set

_∨_

∨-intro₀

∨-intro₁

∨-elim : ∀ {P Q} {R : Set} -> (P -> R) -> (Q -> R) -> (P ∨ Q -> R)

: 是类型定义
val n : Int 这种

∀ 是 forall 

2·2 = 2 + 2

(P -> R) -> (Q -> R) -> (P ∨ Q -> R)

∨-elim pr _ (∨-intro₀ p) = pr p
∨-elim _ qr (∨-intro₁ q) = qr q

(P -> R) -> (Q -> R) -> (P ∨ Q -> R)
   pr    ->    _     -> (∨-intro₀ p) -> R            

(P ∨ Q -> R)

rev : ∀ {n m} {A : Set n} -> Vec A m -> Vec A m

#!/usr/bin/env python3
# -*- encoding: utf-8 -*-

import time
import tgcrypto

FIRST_NAME = '[%H:%M CST] /dev/lwl12'
LAST_NAME = '$' # Follow the rules of Python's strftime

START_TIME = time.time()

from pyrogram import Client, api

def update_name(client):
    client.send(
        api.functions.account.UpdateProfile(
            first_name=time.strftime(FIRST_NAME, time.localtime()),
            last_name=time.strftime(LAST_NAME, time.localtime()) # Change this if you want to use any other timezones
        )
    )
    print('>>> Name updated.')

if __name__ == '__main__':
    app = Client("/home/pi/timeNick/real-time-nick", api_id=114514, api_hash="1919810")
    with app:
        update_name(app)
        quit()

            if (startHour == 0 &&
                startMinute == 0 &&
                endHour == 0 &&
                endMinute == 0) {
                alwaysStatus = getString(R.string.accept_time_card_current_never)
            }

     fun IntArray.allZeros() = this.all { x -> x == 0 }
     if (intArrayOf(startHour, startMinute, endHour, endMinute).allZeros())
       alwaysStatus = getString(R.string.accept_time_card_current_never)      

            if (fileUri == null || !zipFile.exists()) {
                throw NullPointerException()
            }

         if (mGetTopicListCall != null) {
            (mGetTopicListCall as Call<MutableList<Topic>>).cancel()
            mGetTopicListCall = null
        }

mGetTopicListCall 

mGetTopicListCall.cancel() 

mGetTopicListCall

mGetTopicListCall

mGetTopicListCall

        val list = Stream.of(originalList)
                .peek(object : Consumer<Topic> {
                    override fun accept(topic: Topic?) {
                        topic!!.subscribed = (localSubscribedTopics.contains(topic.id))
                    }
                })
                .collect(Collectors.toList())