dhilst

from typing import *
import ast
from dataclasses import dataclass

@dataclass(frozen=True)
class FuncSig:
    name : str
    args : list[str]
    ret: str

dhilst

open Printf

type term = F of string * (term list) | V of string

let rec subst term ((name, replacement) as sub) =
  match term, name with 
  | V x, V y when String.equal x y -> replacement
  | V x, V y when not (String.equal x y) -> term
  | F (x, args), V y -> F (x, List.map (fun arg -> subst arg sub) args)
  | _, _ -> assert false

dhilst

(* A possibly correct unification algorithm implementaion *)
open Printf

type term = F of string * (term list) | V of string

let rec subst subs = function
  | V x -> List.fold_left (fun acc (s, t) -> if x = s then t else V x) (V x) subs 
  | F (x, args) ->
    F (x, 
       List.map (fun arg -> subst subs arg) args)

dhilst

def gen(start, f):
    return lambda: (start, gen(f(start), f))

def inc(a):
    return a + 1

g = gen(0, inc)
while True:
    x, g = g()
    print(x)

dhilst

--- cpdt/src/DataStruct.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/DataStruct.v	2021-12-05 11:05:01.000000000 -0300
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Arguments Nil [A].
-Arguments First [n].
+Arguments Nil {A}.
+Arguments First {n}.

dhilst

from ast import *


class LetVisitor(NodeTransformer):
    def visit_Call(self, node):

        self.generic_visit(node)

        if (
            type(node.func) is Call

dhilst

(* this is the commutativity on Nat.add (the builtin + in Coq) that only simplifies
   from the left *)
Theorem add_comm : forall (n m : nat), n + m = m + n.
  assert (plus_0_r : forall (n' : nat), n' + 0 = n').
  { induction n'. reflexivity. simpl. rewrite IHn'. reflexivity. }
  induction n, m; try reflexivity; simpl; try rewrite plus_0_r; try reflexivity.
  - rewrite IHn. simpl.
    assert (plus_m_Sn : forall (o p : nat), o + S p = S (o + p)).
    { induction o; intros; simpl; try reflexivity. rewrite IHo. reflexivity. }
    rewrite plus_m_Sn. reflexivity.

dhilst

module Foo where

import           Control.Monad.State
{-# ANN module ("hlint: ignore Use <$>") #-}
-- This ^ line disables it 


foo :: State Int String
foo = do
  x <- get

dhilst

using System;

namespace TodoApi
{
    /// <summary>
    /// A generic result class that should enough
    /// to get rid of exceptions and be general enough
    /// for handling all kind of errors.
    ///
    /// User is forced to handle error case to get success

dhilst

function MyClass() abort
  let this = {}

  function this.setA() dict
    let self.a = 1100
  endfunc

  function this.method() dict
    return self.a
  endfunc