PhotonQuantum

open Lean Meta Elab Tactic in
def clearInaccessibles (mvarId : MVarId) : TacticM MVarId := do
  let mvarDecl ← mvarId.getDecl
  let mut lctx  := mvarDecl.lctx
  let mut info  := #[]
  let mut found : NameSet := {}
  let n := lctx.numIndices
  for i in [:n] do
    let j := n - i - 1
    match lctx.getAt? j with

PhotonQuantum

// This theme is from https://github.com/andreasKroepelin/polylux/blob/main/themes/simple.typ
// Author: Andreas Kröpelin

#import "@preview/touying:0.5.3": *
#import themes.simple: *

// https://forum.typst.app/t/how-to-auto-size-text-and-images/1290
#let fill-height-with-text(min: 0.3em, max: 5em, eps: 0.1em, debug: false, it) = layout(size => {
  let fits(text-size, it) = {
    measure(width: size.width, {

PhotonQuantum

#!/usr/bin/env bash
set -euo pipefail
COMPCERT_SRC=~/temp/CompCert-3.7
CTAGS_DEFINITION=/Users/lightquantum/.config/coq.ctags

# Generate tags for Compcert + stdlib + all files under cwd
IFS=" " read -r -a loadpath <<< "$(echo 'Print LoadPath.' | coqtop 2>/dev/null | python loadpath.py)"
find . ${loadpath[@]} $COMPCERT_SRC -type f -name "*.v" -print0 | xargs -0 ctags --options=$CTAGS_DEFINITION

PhotonQuantum

[@@@warnerror "-unused-value-declaration"]

open Bindlib

let ( <.> ) f g x = f (g x)
let ( <..> ) f g x y = f (g x y)

module Mu (M : sig
  type 'fix t
end) =

PhotonQuantum

[@@@warnerror "-unused-value-declaration"]

module type Functor = sig
  type ('p, 'fix) t

  val fmap : ('a -> 'b) -> ('p, 'a) t -> ('p, 'b) t
end

let ( <.> ) f g x = f (g x)

PhotonQuantum

#!/usr/bin/env bash
set -e

declare -A replace_map
replace_map["cargo"]="genshin"
replace_map["Cargo"]="Genshin"
replace_map["rust"]="mihoyo"
replace_map["Rust"]="miHoYo"
replace_map["RUST"]="MIHOYO"

PhotonQuantum

use std::net::TcpListener;
use std::sync::mpsc::{channel, Sender};
use std::thread;
use std::time::Duration;

use futures_util::{SinkExt, StreamExt};
use tungstenite::accept;
use tungstenite::Message;

fn block_client() {

PhotonQuantum

use std::time::Duration;

use actix::{Actor, Arbiter, AsyncContext, Context, System};

struct MyActor;

impl Actor for MyActor {
    type Context = Context<Self>;
    fn started(&mut self, ctx: &mut Self::Context) {
        ctx.run_later(Duration::from_secs(1), |_, _| {

PhotonQuantum

#![feature(bool_to_option)]

use serde::Deserialize;
use std::path::PathBuf;
use regex::Regex;
use std::fs::{read_dir, File};
use opencc_rust::*;

#[derive(Debug, Deserialize)]
struct Poetry {

PhotonQuantum

标记说明：

A 课程类型：主修、民族课、版块课（体育，英语）等，影响 rwlx xkly xkkz_id bklx_id kklxdm
B 个人及客观信息：学期号、专业号、选课学年等
C 特定课程及教学班信息
E 请求相关：分页参数

静态网页及相应查询参数准备

A1. 请求所有课程类型