Comments (1)
Nils Anders Danielsson [email protected] writes:
The code below is rejected:
module test where import prelude import nat foo : nat = undefined fooIsFoo : Id nat foo foo = refl nat foo
Error message:
eval: undefined at test_L6_C13
Why are you evaluating
foo
?Thanks for reporting. How type-checking is done currently, terms are
checked against values. So after the typeId nat foo foo
is checked,
its value is added to the type-checking context; herefoo
gets
evaluated. A quick fix for this particular problem is to evaluate
undefined into a closure. (pushed)-- Simon
from cubicaltt.
Related Issues (20)
- New lines when printing systems HOT 3
- boundaries of nested splits HOT 1
- Add command-line options to run commands (or take a command file) and/or redirect output HOT 7
- cubical.exe does not support {- -} comments HOT 2
- Problem with parser generated by bnfc HOT 4
- Doesn't work on M1 Mac
- cubicaltt crashes when replacing an 'undefined' with a 'hole'.
- Bound Check Error HOT 1
- A pattern matching for predicate function HOT 5
- Bracket matching of \(x : A) HOT 1
- Document opaque / transparent HOT 1
- Does indent matter in cubicaltt? HOT 4
- Allow opaque/transparent in the command line
- Layout errors crash REPL
- Path completion in :l
- missing dependencies of experiments/truncS2.ctt HOT 1
- Evaluation priority idea
- Parser error messages are truncated too much HOT 5
- Hopf Fibration HOT 12
- Etale Map 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
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 ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.
from cubicaltt.