msmorgan

module Data.AltList

%access public export
%default total

data AltList : (a : Type) -> (b : Type) -> Type where
  Nil : AltList a b
  ConsB : b -> AltList a b -> AltList a b
  ConsAB : a -> b -> AltList a b -> AltList a b

msmorgan

module Data.ToggleList

%access public export
%default total

data Next = A | B

next : Next -> Type -> Type -> Type
next A a _ = a
next B _ b = b

msmorgan

data CloserToZero : Integer -> Integer -> Type where
  CTZ : So (x * x < y * y) -> CloserToZero x y

CTZInj : CloserToZero x y -> So (x * x < y * y)
CTZInj (CTZ oh) = oh

closerToZero : (x, y : Integer) -> Dec (CloserToZero x y)
closerToZero x y with (x * x < y * y) proof prf
  closerToZero x y | True = Yes (CTZ (rewrite sym prf in Oh))
  closerToZero x y | False = No (absurd . the (So False) . rewrite prf in CTZInj)

msmorgan

module SParser

import Text.Lexer
import Text.Parser

data SParser : Type -> Type -> Bool -> Type -> Type where
  MkSParser : (s -> Grammar t c (a, s)) -> SParser s t c a

Functor (SParser s t b) where
  map f (MkSParser g) = MkSParser $ \s => map (\(v,s) => (f v, s)) (g s)

msmorgan

  term : MRule Expr
  term = pure $ let (x, xs) = !multChain in
                    foldl (Binary Mul) x xs
    where
      multChain : MRule (Expr, List Expr)
      multChain = do x <- factor
                     xs <- (do let op = match (Op Mul)
                               op
                               commit
                               sepBy1 op factor) <|> pure []

msmorgan

-0/-1
-0/-2
-1/-0
-1/-1
-2/-1
-2/-2
+0/+1
+0/+2
+1/+0
+1/+1

msmorgan

use std::collections::HashSet;

use serde::{Deserialize, Serialize};

struct Context {
    applications: HashSet<String>,
}

impl Context {
    pub fn new() -> Self {

msmorgan

class A {
  final name = 'A';
  
  void printName() {
    print(name);
  }
}

class B extends A {
  @override

msmorgan

from itertools import accumulate


MONTH_NAMES = ['Jan', 'Feb', 'Mar', 'Apr', 'May', 'Jun', 'Jul', 'Aug', 'Sep', 'Oct', 'Nov', 'Dec']
MONTH_LENGTHS = [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31]
MONTH_STARTS = list(accumulate([0] + MONTH_LENGTHS[:-1]))  # [0, 31, 31+28, 31+28+31, ...]


def is_leap_year(year: int) -> bool:
    return year % 4 == 0 and (year % 100 != 0 or year % 400 == 0)