alok

inductive Transcendental where
  | sin
  | cos
  | tan
  | exp
  | log
  deriving Repr

/-- A simple vector type with a proof that the size is the same as the length of the array-/
structure Vector (a : Type) (n : Nat) where

alok

import Lean.Parser
import Std.Internal.Parsec
import Std.Data.HashMap
open Lean.Parser

open Std.Internal.Parsec

/-!
{- GTX: custom document format for Gwern.net, for lightweight writing of annotations.

alok

author	Alok Singh
comments	true
layout	post
mathjax	true
slug	noncommutative-3d-rotations
title	Exploring Non-Commutative 3D Rotations with Grassmann Algebra

People find rotation hard because when we try to visualize something, often we project it onto a 2D plane. But for rotations, this loses the plot because 2D rotations DO commute. In this post, we will (symbolically) explore this non-commutative nature of 3D rotations using Grassmann algebra in Julia. We'll use the Grassmann package to define rotors and demonstrate how the order of rotations matters in three-dimensional space.

alok

import Mathlib
import Lean.Data.Parsec
import Batteries.Lean.HashMap
import Lean.Data.HashMap

import Lean.Util.Path
import Lean.Data.Rat
import LeanInf.Basic
-- set_option diagnostics true
theorem two_plus_two : 2 + 2 = 4 := rfl

alok

import Lean
import Lean.Parser
import Mathlib
open Lean.Parsec

namespace Lisp
-- Lisp data types
inductive LispVal where
  | Atom (name : String)
  | List (elements : List LispVal)

alok

# Reorganized code to focus on rotating a random 17-dimensional multivector and projecting it to 3D for visualization

using Grassmann

# Define the basis for 3D and 17D spaces
basis_3,basis_5,basis_17 = Λ(3), Λ(5), Λ(17)

# Define submanifolds for 3D and 17D spaces
V_3, V_5, V_17 = Submanifold(3), Submanifold(5), Submanifold(17)

alok

inductive Format :=
  | Int (rest: Format) -- %d
  | String (rest: Format) -- %s
  | Other (char: Char) (rest: Format) -- %c
  | End


def format : List Char -> Format
  | ('%' :: 'd' :: cs) => .Int (format cs)
  | ('%' :: 's' :: cs) => .String (format cs)

alok

"""
Configuration example for ``ptpython``.
Copy this file to ~/.ptpython/config.py
"""
from __future__ import unicode_literals

from prompt_toolkit.keys import Keys
from ptpython.layout import CompletionVisualisation
from pygments.token import Token

alok

{
  "global": {
    "check_for_updates_on_startup": true,
    "show_in_menu_bar": true,
    "show_profile_name_in_menu_bar": false
  },
  "profiles": [
    {
      "complex_modifications": {
        "rules": [

alok

{
  "global": {
    "check_for_updates_on_startup": true,
    "show_in_menu_bar": true,
    "show_profile_name_in_menu_bar": false
  },
  "profiles": [
    {
      "complex_modifications": {
        "rules": [