- telescope of Nat
- ⊢
Type
- result ⊢
Type
↑ Type
- result ⊢
- ⊢
- telescope of zero
- zero
- telescope of Nat
- ⊢
Type
- result ⊢
Type
↑ Type
- result ⊢
- ⊢
- telescope of suc
- ⊢
Nat
: Type
- ⊢
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- twitter thread: https://twitter.com/EgbertRijke/status/1349865209591173120 | |
{-# OPTIONS --cubical #-} | |
open import Cubical.HITs.PropositionalTruncation using (∥_∥; ∣_∣; squash; rec) | |
open import Cubical.Relation.Nullary | |
open import Cubical.Foundations.Function using (_∘_; idfun) | |
open import Cubical.Data.Sigma using (_×_; fst; snd) | |
import Cubical.Data.Empty as ⊥ using (elim) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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;} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 ε |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 -> ℕ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![allow(dead_code)] | |
#[derive(Default)] | |
pub struct Schema { | |
fields: Vec<String>, | |
} | |
pub struct Order(); | |
macro_rules! impl_node { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
\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)} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |