alcides

import tactic.suggest
import tactic.basic
import smt

open smt_tactic

set_option pp.all true

lemma example_of_something_for_which_smt_is_useful 
        (f : list nat → list nat) (a b c : list nat) :

alcides

import importlib

class MyError(Exception):
    pass
    
    def __str__(self):
        return "HERE"

try:
    print("hi")

alcides

# Depende do Lark: pip3 install lark-parser

import os
import sys
from lark import Lark
from lark.lexer import Token


def get_contents(fname):
    return open(fname).read()

alcides

from z3 import *
from itertools import combinations

s = Solver()


h1, h2, h3, h4, l, b1, b2 = Ints("h1 h2 h3 h4 l b1 b2")
hippos = [h1, h2, h3, h4]

for w in [223,235,248,272]:

alcides

package com.alcidesfonseca.llvmgenerator;

/*
 * Helper functions to convert float and double constants to LLVM format
 * 
 * Inspired by Scala Native
 * */

public class ConstantUtils {
	public String floatToLLVM(float f) {

alcides

from z3 import *

y,g,r,b = Ints("y g r b")
c1, c2, c3, c4 = Ints("c1 c2 c3 c4")

s = Solver()
for v in [y,g,r,b]:
    s.add(z3.And(v > 0, v < 10))
    
    

alcides

import Base.+
import Base.-
import Base.<
import Base.Meta.@lower

struct Refined{T, cond} # <: T where {T <: Number} 
   e::T
   Refined{T, cond}(x::T) where {T, cond} = new{T, cond}(x)
end

alcides

import javafx.application.Application;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.layout.StackPane;
import javafx.stage.Stage;
 
public class HelloWorld extends Application {
    

alcides

/*

A solution for the "Vasco Vasconcelos Petition challenge", using rust mpsc package.

Alcides Fonseca <[email protected]>

How to run:
rustc example.rs && ./example

*/

alcides

"""

Doc: 

https://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.18.2

If an integer addition overflows, then the result is the low-order bits of the mathematical sum as represented in some sufficiently large two's-complement format.

"""