max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(kernel/expr): constructor order

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 15:56:51 -07:00
parent 45202eca16
commit 0119926022
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/expr.h
View file

@ -45,7 +45,7 @@ class expr;
| Let name expr expr expr
| Macro macro
*/
enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Let, Macro };
enum class expr_kind { Var, Local, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro };
class expr_cell {
protected:
// The bits of the following field mean:

2
src/library/vm/vm.h
View file

@ -55,7 +55,7 @@ public:
#if defined(LEAN_VM_UNCHECKED)
#define lean_vm_check(cond) lean_assert(cond)
#else
#define lean_vm_check(cond) { if (LEAN_UNLIKELY(!(cond))) vm_check_failed(#cond); }
#define lean_vm_check(cond) { lean_assert(cond); if (LEAN_UNLIKELY(!(cond))) vm_check_failed(#cond); }
#endif
void display(std::ostream & out, vm_obj const & o);