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.

ice1000

package org;
// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
// Use of this source code is governed by the GNU GPLv3 license that can be found in the LICENSE file.

import java.util.*;
import java.util.stream.Collectors;


/**
 * @author danihao123

ice1000

\newcommand{\lrbracket}[1]{\llbracket #1 \rrbracket}
\newcommand{\Tm}[2]{\text{Tm}(#1, #2)}
\newcommand{\FF}{\mathcal F}
\newcommand{\CC}{\mathcal C}
\newcommand{\EE}{\mathcal E}
\newcommand{\lrangle}[1]{\langle#1\rangle}
\newcommand{\Prop}{\text{Prop}}
\newcommand{\El}[1]{\text{El}(#1)}
\newcommand{\eqlzSimp}{\mathrm{eq}}
\newcommand{\eqlz}[2]{\eqlzSimp(#1,#2)}

ice1000

import java.util.List;
import java.util.Map;
public class Main {
	interface Level {
		// Pattern matcher
		interface Visitor<P, R> {
			R visitConst(Const c, P p);
			R visitInfinity(P p);
			R visitRef(Reference r, P p);
		}