WorldSEnder

use gloo_events::EventListener;
use wasm_bindgen::{JsCast, UnwrapThrowExt};
use yew::events::{Event, KeyboardEvent};
use yew::html::IntoPropValue;
use yew::prelude::*;
use yew::virtual_dom::VNode;

#[derive(Copy, Clone, Debug, PartialEq)]
pub enum TooltipPosition {
    Top,

WorldSEnder

use gloo_console as console;
use js_sys::Date;
use std::rc::Rc;
use yew::{function_component, html, use_reducer, Callback, Html, Reducible};

// Define the possible actions which can be sent to the counter
pub enum Action {
    Increment,
    Decrement,
}

WorldSEnder

#![feature(generators, generator_trait, never_type, type_alias_impl_trait)]

use yew::html::AnyScope;
use pin_cell::PinMut;
use pin_cell::PinCell;
use std::rc::Rc;
use std::pin::Pin;
use yew::Html;
use yew::Component;
use yew::ComponentLink;

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")

WorldSEnder

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

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

{-# 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

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 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

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: