kiranandcode

(library
 (name macros)
 (modules "macros")
 (libraries ppxlib)
 (kind ppx_rewriter)
 (preprocess (pps ppxlib.metaquot)))

(executable
 (public_name macros)
 (modules "main")

kiranandcode

import Batteries
import Lean.Elab.BuiltinEvalCommand

open Lean.Meta Lean.Elab

-- Most of this stolen from Lean/Elab/BuiltinEvalcommand.lean

/--
Try to make a `@projFn ty inst e` application, even if it takes unfolding the type `ty` of `e` to synthesize the instance `inst`.
-/

kiranandcode

kiranandcode

kiranandcode

#lang racket

(require (for-syntax syntax/parse
                     racket/syntax
                     racket/string
                     racket/match
                     syntax/parse/class/paren-shape))
(provide make-godot-parser define-godot-bindings)

(module+ test

kiranandcode

"========== character a ============"
mathcomp.solvable.abelian.html contains: 
 - end :  Q16220058
 - order :  Q2029226
 - structure :  Q6671777
 - f :  Q9765
 - g :  Q9739
 - t :  Q9813
 - d :  Q9884
 - call :  Q407264

kiranandcode

;;; search-with-llama.el --- Find an answer to your query using llama!  -*- lexical-binding: t; -*-

;; Copyright (C) 2023  Kiran Gopinathan

;; Author: Kiran Gopinathan
;; Keywords: 

;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or

kiranandcode

;;; cram-mode.el --- Emacs mode for CRAM tests            -*- lexical-binding: t; -*-

;; Copyright (C) 2023  Kiran Gopinathan

;; Author: Kiran Gopinathan
;; Keywords: 

;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or

kiranandcode

use std::ops::{Add, AddAssign, Sub};
pub trait Lerpable<T> {
    fn at_progress(&self, progress: f32) -> T;
}
pub trait Diffable<T, U : Lerpable<T>> {
    fn diff(start: &T, end: &T) -> U;
}


pub struct AddativeDiff<T, U : Lerpable<T>> {

kiranandcode

#[macro_use] extern crate dependent_view;

use std::rc::{Weak, Rc};
use dependent_view::rc::DependentRc;

trait Testable {
    fn get_id(&self) -> usize;
    fn get_i_id(&self) -> usize;
}