Crate formality_core

Expand description

formality-core contains core definitions that can be used for languages that are not Rust. It is intended to play a role similar to

Modules§

bail: Return early with an error.
cast_impl
debug: Constructs an event at the debug level.
declare_language: Declares a new formality language. This will generate a module with a name you choose that contains various items; among them will be a struct named FormalityLang that implements the Language trait. When you use the auto-derives or the term macro, they will generate code that references crate::FormalityLang, so you need to bring that in scope at the root of your crate (e.g., if you called the module mylang, you might add use crate::mylang::FormalityLang at the root of your crate, so that the auto-derives can find it.)
id: Declares a newtyped struct that is an arbitrary (string) identifier, like the name of a module or something.
judgment_fn
push_rules: push_rules! allows construction of inference rules using a more logic-like notation.
seq: Replacement for the vec macro that supports ..foo notation to flatten vectors.
set
trace: Constructs an event at the trace level.
trait_alias

Deduplicate
Downcast: This is the convenience trait whose method you should call to do a downcast.
DowncastFrom: Our version of “try-from”. A “downcast” casts from a more general type (e.g., any Parameter) to a more specific type (e.g., a type). This returns an Option because the value may not be an instance of the more specific type.
DowncastTo: Our version of “try-into”. A “downcast” casts from a more general type (e.g., any Parameter) to a more specific type (e.g., a type).
Downcasted
SetExt
To
Upcast: Our version of Into. This is the trait you use in where clauses, but you typically implement UpcastFrom.
UpcastFrom: Our version of From. One twist: it is implemented for &T for all T. This is the trait you implement.
Upcasted

with_tracing_logs: Run an action with a tracing log subscriber. The logging level is loaded from RUST_LOG. The formality_macro::test expansion uses this to enable logs.

fixed_point
instrument: Instruments a function to create and enter a tracing span every time the function is called.
requires: Pre-conditions are checked before the function body is run.
term
test