@JvmName
@JvmStatic
@JvmField
@file:JvmName
@PureReified
@Contract

open class A {
    open fun f() { print("A") }
    fun a() { print("a") }
}

interface B {
    fun f() { print("B") } // interface members are 'open' by default
    fun b() { print("b") }
}

class C() : A(), B {
    // The compiler requires f() to be overridden:
    override fun f() {
        super<A>.f() // call to A.f()
        super<B>.f() // call to B.f()
    }
}

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()