lf94

Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) ->
b = c.

Proof.
intros b c.
destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.

lf94

"Strings" form a group

By the end of this, we will have defined insert, delete, find and replace operations.

Talking about polymorphism with someone in the context of JS, the following example came up:

lf94

.intel_syntax noprefix

.include "std.macro"
.include "curl.const"

  .section .data
curl:       .quad 0

  .section .rodata
url_google: .asciz "http://google.com"

lf94

.intel_syntax noprefix

.include "std.macro"

  .section .text
fib: op1 = rdi; op2 = rsi; iterations = rcx
  xadd op2, op1
  loop fib
  ret
  

lf94

// Propositional logic implemenation
const True  = a => b => a;
const False = a => b => b;
const If    = x => x;
const Not   = a => a(False)(True);
const And   = a => b => a(True)(False)(b(True)(False))(False);
const Or    = a => b => a(True)(b(True)(False));
const Xor   = a => b => And(Or(a)(b))(Not(And(a)(b)));

// SKI calculus implementation

lf94

def toAddress(bytes):
    return int.from_bytes(bytes, byteorder='big')

class Map:
    # Map structure is tied to a file
    def __init__(self, fileHandle):
        self.fileHandle = fileHandle
        self.header = self.Header(fileHandle)
        fileHandle.seek(toAddress(self.header.commands[-1].data))
        self.mesh = Mesh(fileHandle)

lf94

trait Component {
  fn draw(&self, ctx: &mut Context) -> ();
  fn get_children(&self) -> Vec<Component>;
}

struct Label {
  children: Vec<Component>,
  text: graphics::Text,
  color: graphics::Color,
  position: graphics::Point,

lf94

{ (include './contract.lll'

  (def 'enough-paid (>= callvalue required-amount))
  (def 'enough-betters (>= number-of-betters required-betters))
  (def 'is-paying-out (= paying-out 1))

  (def 'minimum-bet-amount 10) ; Wei
  (def 'required-betters 10)

  (init {

lf94

pub fn nth(n: usize) -> Result<u64, &'static str> {
  if n <= 0 { Err("No primes below 1") }
  else {
    match (2..).filter(|&x| is_prime(x)).nth(n - 1) {
      Some(n) => Ok(n),
      None => Err("Iteration error")
    }
  }
}

lf94

pub fn reply(message: &str) -> &str {
  let chrs          = || message.trim().chars();
  let has_text      = chrs().any(|c| c.is_alphanumeric());
  let has_letters   = chrs().any(|c| c.is_alphabetic());
  let has_lowercase = chrs().any(|c| c.is_alphabetic() && !c.is_uppercase());
  
  if has_letters && has_text && !has_lowercase { "Whoa, chill out!" }
  else if chrs().as_str().ends_with("?") { "Sure." }
  else if !has_text { "Fine. Be that way!" }
  else { "Whatever." }