ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.Int
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.SetTruncation

-- Maps out of a set-truncated int can only target sets,
-- yet it's equivalent to the normal int

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.List
open import Cubical.Data.Nat.Base
open import Cubical.Data.Equality hiding (map)

variable
  A : Type
  B : Type
  n : ℕ

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.Vec
open import Cubical.Data.Nat.Base
open import Cubical.Data.Equality hiding (map)

variable
  A : Type
  B : Type
  n : ℕ

ice1000

public interface GADT {
  // Self-indexed natural numbers
  sealed interface Nat<T extends Nat<T>> {
    Nat<T> self();
  }
  record Z() implements Nat<Z> {
    public Z self() {return this;}
  }
  record S<T extends Nat<T>>(Nat<T> pred) implements Nat<S<T>> {
    public S<T> self() {return this;}

ice1000

C:\Java\LibericaJDK-19\bin\java.exe --enable-preview ... -m aya.cli.console/org.aya.cli.console.Main test.aya --pretty-dir=out --pretty-stage=typed --pretty-format=html
In file test.aya:116:4 ->

  114 │   | Γ ▷ A => Sig (Γw : WfCon Γ) ** (WfTy Γ Γw A)
  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
      │       ╰──╯

Error: Unhandled case:
         Γ, _5, {Γ'}, Subst U ε

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.Nat.Base hiding (_∸_)
open import Cubical.Core.Everything

data Andrej : Set where
  Tesla Zhang : ℕ -> Andrej
  Bauer : Tesla 7 ≡ Zhang 6

demo : Andrej -> ℕ

ice1000

• telescope of Nat
  • ⊢ Type
    • result ⊢ Type ↑ Type
• telescope of zero
• zero
• telescope of Nat
  • ⊢ Type
    • result ⊢ Type ↑ Type
• telescope of suc
  • ⊢ Nat : Type

ice1000

diff --git a/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java b/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java
new file mode 100644
index 0000000..8ef920c
--- /dev/null
+++ b/base/src/main/java/org/aya/guest0x0/syntax/BdryData.java
@@ -0,0 +1,32 @@
+package org.aya.guest0x0.syntax;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;

ice1000

#![allow(dead_code)]

#[derive(Default)]
pub struct Schema {
    fields: Vec<String>,
}

pub struct Order();

macro_rules! impl_node {

ice1000

#![allow(dead_code)]
#![allow(unused_parens)]
#![allow(unused_variables)]

pub struct Schema {
    /// name of each column
    pub fields: Vec<String>,
}

/// the `RelationalOperator` represent operator whose output is relation.