Comments (7)
…you need to pattern match on
x.fst
,x.snd
, etc.
This isn't possible in data definitions…
from aya-dev.
I think there isn't a syntax for that
from aya-dev.
You should use projections on structs.
from aya-dev.
We will now report an error for this code (instead of throwing exceptions)
from aya-dev.
But how to use projections in patterns? Sorry if this is a stupid question.
from aya-dev.
But how to use projections in patterns? Sorry if this is a stupid question.
I mean you need to pattern match on x.fst
, x.snd
, etc. But then you need to create new functions to pattern match on 'em. Sorry, the syntax is stupid, but we haven't decided on how to implement pattern matching expressions.
from aya-dev.
…you need to pattern match on
x.fst
,x.snd
, etc.This isn't possible in data definitions…
open data U2Impl (x y : Bool) : Set
| false, false => zero
| false, true => one
| true, false => two
| true, true => three
def U2 (x : BoolPair) => U2Impl x.fst x.snd
from aya-dev.
Related Issues (20)
- StackOverflow HOT 1
- DSL for generating highlighted contents
- bors is dead, what to do? Enable GHMQ? HOT 4
- Goal didn't give reasonable types HOT 1
- `IndexOutOfBoundsException` when parsing result types HOT 4
- Crash with `InternalException` after report an error HOT 3
- Wrong URL to CI badge
- Container image for Aya HOT 5
- Unification bug
- We should use `enum X { Obj; }` for singletons! HOT 1
- Literate mode bug? HOT 2
- Fully predicative termination checker
- Type Infering HOT 1
- Bad Meta HOT 7
- We should develop our own IDE HOT 6
- Markdown backend bug HOT 1
- `atob` seems broken in vuepress HOT 7
- We need a better literate backend for academic writing HOT 4
- `aya-hidden` is printed to tex HOT 2
- InternalException about Generalized Variables HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from aya-dev.