WorldSEnder

pkgname=HyPro
pkgdesc="A C++ state set representation library for the analysis of hybrid systems"
url="https://github.com/hypro/hypro"
arch=("i686" "x86_64")
license=("mit")
depends=("gmp" "boost" "glpk" "carl")
makedepends=("make" "cmake")
conflicts=()
replaces=()
backup=()

WorldSEnder

pkgname=carl
pkgdesc="An Open Source C++ Library for Computer Arithmetic and Logic"
url="https://github.com/smtrat/carl"
arch=("i686" "x86_64")
license=("mit")
depends=("gmp" "eigen3" "boost")
makedepends=("make" "cmake")
conflicts=()
replaces=()
backup=()

WorldSEnder

#include <iostream>

class Foo {
    int bar = 0;
    int foobar = 999;
    static inline int zip;
public:
    void print() {
        std::cout << "Bar: " << bar << std::endl;
        std::cout << "Zip: " << zip << std::endl;

WorldSEnder

import sys, errno, io
import struct
import base64

import blowfish

key = base64.b64decode(b'eGllWmpvZSNQMjEzNC0zem1hZ2hncHFvZTB6OCQzYXplcQ==')
cipher = blowfish.Cipher(key, byte_order="little")

if sys.version_info[0] == 3:

WorldSEnder

{-# OPTIONS --cubical #-}

module modularAutomata where

open import Data.Maybe
open import Cubical.Data.Prod
open import Cubical.Foundations.Everything

-- first, setup a type of infinite (coinductive) lists, we will need it later for simulation
record νList (A : Set) : Set where

WorldSEnder

module braunTree where

open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Empty
open import Data.List
open import Level
open import Function

data Tree {a} (A : Set a) : Set a where

WorldSEnder

{-# OPTIONS --cubical #-}

module UniverseSIP where

open import Cubical.Data.Prod
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Core.Glue

WorldSEnder

{-# OPTIONS --cubical #-}
{-

This module shows a few syntactical additions, that, like Setoid reasoning in the standard library,
are supposed to make logical reasoning more readable. One of the goals is to avoid having to write
`PropositionalTruncation.rec squash` everywhere when "unpacking" a truncated datatype.

`obtain n ∶ A by prf - cont` does just that. It takes a "proof" producing a truncated ∥ A ∥ and
makes an untruncated A available in the context of cont. There is a special version for mere existance
of an element with a certain property making the property available as a "tactic":

WorldSEnder

{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, PolyKinds, UndecidableSuperClasses #-}
{-# LANGUAGE Rank2Types, TypeApplications, QuantifiedConstraints #-}
module TaggingDefs
( Tagged(..)
, Untag
, Retag
, untag
, untag'
, retag
, retag'

WorldSEnder

pkgname=idris2
pkgver=0.2.1
pkgrel=1
pkgdesc="Funtional Programming Lanugage with Dependent Types"
url="https://www.idris-lang.org/"
license=('custom')
arch=('x86_64')
depends=('chez-scheme')
makedepends=('git')
source=("https://www.idris-lang.org/idris2-src/idris2-$pkgver.tgz")