WorldSEnder

// The two main components are the interfaces
// Generic<T, Context> and GenericArg<"identifier">

// Generic basically structurally replaces types in T that are GenericArg<S>
// for some `S extends keyof Context` with `Context[S]`
// See the test cases for specific uses.

// ====== TESTING
// Pass through for trivial types
type Test00 = Generic<number>;

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