Comments (1)
I think in Coq there is a separate Prop
universe for proof irrelevant (erasable) propositions. So maybe you could also have an universe for those, such that Equal(A,a,b) : Prop
. I have no idea about the details of that though, it's still something I'm trying to learn myself.
Another approach would be primitive or user-defined rewrite rules, so that Equal.rewrite(e, x) ~> x
. Though I guess that will make type preservation (aka subject reduction) fail.
Note that it's only type-safe to erase proofs if the type theory is consistent. Else I could just proof A = B
with an infinite loop and then cast A
to B
freely (if the proof was erased). So the proof cannot be erased so that if you have an invalid proof A = B
then at least you will get an infinite loop when you try to cast A
to B
.
See this stackoverflow question for a nice answer.
from kind.
Related Issues (20)
- LLM Support HOT 1
- Bump version to 0.1.2
- Bump cli version to 0.3.8
- Bump cli version to 0.3.9
- "New Type" Optimization
- Improve error messages by removing things like implicit arguments
- Add type checker for erased Pi, App and Lam
- Remove old parser and stuff to use treesitter
- Add new type of error messages used for LLMs.
- error[E0599]: no method named `as_ptr` found for struct `AtomicU64` in the current scope HOT 2
- Add an API for cursor on trees
- Add slash on the end of identifiers as another type of "use"
- Add flag to remove dependency errors
- New panic hook for the language.
- Add flag to show immediate dependencies
- Inconsistency in type check messages
- Update basic function names for Kindex update HOT 1
- Create a project/package manager
- Refactor file loading and name resolution module
- Compiler crashes when using an undeclared alias
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 kind.